# HG changeset patch # User Chris Cannam # Date 1498559450 -3600 # Node ID 1f4fb4a0f62aad2cd7a7dad98222678a399408b6 # Parent e64981b88943aaf2c57244d0cc0f3169c5237e21# Parent 434be2f0509e1096fc7693c79666db6b7c8b53d8 Merge from branch output-type-uri diff -r e64981b88943 -r 1f4fb4a0f62a vext --- a/vext Tue Jun 20 11:44:32 2017 +0100 +++ b/vext Tue Jun 27 11:30:50 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