diff repoint @ 346:90169412b1a7

Merge from branch by-id
author Chris Cannam
date Thu, 18 Jul 2019 14:58:51 +0100
parents ba3c0e70b5dd
children
line wrap: on
line diff
--- a/repoint	Fri Sep 14 14:55:24 2018 +0100
+++ b/repoint	Thu Jul 18 14:58:51 2019 +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"