diff repoint @ 258:84de57beb8d6

Update Repoint
author Chris Cannam <cannam@all-day-breakfast.com>
date Mon, 27 Jan 2020 12:34:20 +0000
parents e737931b1925
children
line wrap: on
line diff
--- a/repoint	Mon Jan 27 11:06:42 2020 +0000
+++ b/repoint	Mon Jan 27 12:34:20 2020 +0000
@@ -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"