diff repoint @ 1823:1b6ffed298a2

Update Repoint to v1.0
author Chris Cannam
date Fri, 18 May 2018 13:49:23 +0100
parents adc8a48f4e4c
children
line wrap: on
line diff
--- a/repoint	Fri May 18 13:49:16 2018 +0100
+++ b/repoint	Fri May 18 13:49:23 2018 +0100
@@ -58,7 +58,7 @@
     # That is fixed in v5.7.1, so we could promote it up the order
     # again at some point in future
     elif echo | poly -v 2>/dev/null | grep -q 'Poly/ML'; then
-	sml="poly"
+	sml="polyml"
     elif mlton 2>&1 | grep -q 'MLton'; then
 	sml="mlton"
     # MLKit is at the bottom because it leaves compiled files around
@@ -109,7 +109,7 @@
 done
 
 case "$sml" in
-    poly)
+    polyml)
         if [ -n "$local_install" ] && polyc --help >/dev/null 2>&1 ; then
             if [ ! -x "$gen_out" ]; then
                 polyc -o "$gen_out" "$program"