comparison vext @ 1721:bf8a5ce8fb62 vext

Update vext; providers -> services

 # preference is based on startup speed.
 
 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
 	sml="mlton"
     else cat 1>&2 <<EOF