| changeset 73483 | 804e75127f29 |
| parent 73482 | 9830d7981ad0 |
| child 73509 | 5d750df8e894 |
--- a/lib/Tools/version Sat Mar 27 18:03:50 2021 +0100 +++ b/lib/Tools/version Sat Mar 27 18:15:19 2021 +0100 @@ -67,6 +67,9 @@ HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt" +export LANG=C +export HGPLAIN= + if [ -n "$SHORT_ID" ]; then if [ -d "$ISABELLE_HOME/.hg" ]; then "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?"