more robust invocation of hg;
authorwenzelm
Sat, 27 Mar 2021 18:15:19 +0100
changeset 73738 804e75127f29
parent 73737 9830d7981ad0
child 73739 4f8849357ba7
more robust invocation of hg;
Admin/cronjob/plain_identify
Admin/lib/Tools/churn
Admin/lib/Tools/churn_pie
lib/Tools/version
src/Pure/General/mercurial.scala
--- 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"
--- 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" "$@"
--- 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" "$@"
--- 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 "$?"
--- 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)