# HG changeset patch
# User wenzelm
# Date 1616865319 -3600
# Node ID 804e75127f29580af6377ef4d207be43b456ff2d
# Parent  9830d7981ad0b1e8fd32268fa40002869bc03955
more robust invocation of hg;

diff -r 9830d7981ad0 -r 804e75127f29 Admin/cronjob/plain_identify
--- a/Admin/cronjob/plain_identify	Sat Mar 27 18:03:50 2021 +0100
+++ b/Admin/cronjob/plain_identify	Sat Mar 27 18:15:19 2021 +0100
@@ -7,7 +7,8 @@
 
 source "$HOME/.bashrc"
 
-LANG=C
+export LANG=C
+export HGPLAIN=
 
 REPOS_DIR="$HOME/cronjob/plain_identify_repos"
 ISABELLE_REPOS_SOURCE="https://isabelle.sketis.net/repos/isabelle"
diff -r 9830d7981ad0 -r 804e75127f29 Admin/lib/Tools/churn
--- a/Admin/lib/Tools/churn	Sat Mar 27 18:03:50 2021 +0100
+++ b/Admin/lib/Tools/churn	Sat Mar 27 18:15:19 2021 +0100
@@ -9,4 +9,7 @@
 
 cd "$(dirname "$ALIAS")"
 
+export LANG=C
+export HGPLAIN=
+
 "${HG:-hg}" churn --aliases "$ALIAS" "$@"
diff -r 9830d7981ad0 -r 804e75127f29 Admin/lib/Tools/churn_pie
--- a/Admin/lib/Tools/churn_pie	Sat Mar 27 18:03:50 2021 +0100
+++ b/Admin/lib/Tools/churn_pie	Sat Mar 27 18:15:19 2021 +0100
@@ -11,4 +11,7 @@
 
 cd "$(dirname "$ALIAS")"
 
+export LANG=C
+export HGPLAIN=
+
 "${HG:-hg}" churn --aliases "$ALIAS" | "$SCRIPT" "$@"
diff -r 9830d7981ad0 -r 804e75127f29 lib/Tools/version
--- 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 "$?"
diff -r 9830d7981ad0 -r 804e75127f29 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Mar 27 18:03:50 2021 +0100
+++ b/src/Pure/General/mercurial.scala	Sat Mar 27 18:15:19 2021 +0100
@@ -88,7 +88,7 @@
       repository: Boolean = true): Process_Result =
     {
       val cmdline =
-        "export HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
+        "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
           (if (repository) " --repository " + ssh.bash_path(root) else "") +
           " --noninteractive " + name + " " + options + " " + args
       ssh.execute(cmdline)