# HG changeset patch # User Chris Cannam # Date 1498474463 -3600 # Node ID 434be2f0509e1096fc7693c79666db6b7c8b53d8 # Parent 1db385567addbdcd8a2e9749346ada934680d0e5 Update vext diff -r 1db385567add -r 434be2f0509e vext --- a/vext Tue Jun 20 11:46:04 2017 +0100 +++ b/vext Mon Jun 26 11:54:23 2017 +0100 @@ -16,13 +16,13 @@ # 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 - if echo | poly -v 2>/dev/null | grep -q 'Poly/ML'; then + elif echo | poly -v 2>/dev/null | grep -q 'Poly/ML'; then sml="poly" - elif sml -h 2>&1 | grep -q 'Standard ML of New Jersey'; then - sml="smlnj" elif mlton 2>&1 | grep -q 'MLton'; then sml="mlton" else cat 1>&2 < ERROR e - | OK tid => - OK (tid = id andalso - tid <> id_or_tag) (* else id_or_tag was id not tag *) + ERROR e => OK false (* id_or_tag is not an id or tag, but + that could just mean it hasn't been + fetched *) + | OK tid => OK (tid = id) fun branch_tip context (libname, branch) = git_command_output context libname