diff vext @ 1721:bf8a5ce8fb62 vext

Update vext; providers -> services
author Chris Cannam
date Wed, 28 Jun 2017 13:20:05 +0100
parents 434be2f0509e
children 669bd699082d
line wrap: on
line diff
--- a/vext	Tue Jun 27 14:31:29 2017 +0100
+++ b/vext	Wed Jun 28 13:20:05 2017 +0100
@@ -18,9 +18,10 @@
 if [ -z "$sml" ]; then
     if sml -h 2>&1 | grep -q 'Standard ML of New Jersey'; then
 	sml="smlnj"
-    # I think there may be a race condition in the poly interpreter's
-    # tests for open or closed I/O streams - without the "echo" here,
-    # or with stderr redirection, this pipeline will sometimes hang
+    # We would prefer Poly/ML to SML/NJ, except that Poly v5.7 has a
+    # nasty bug that occasionally causes it to deadlock on startup.
+    # That appears to be fixed in their repo, 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"
     elif mlton 2>&1 | grep -q 'MLton'; then