# HG changeset patch
# User wenzelm
# Date 1375388407 -7200
# Node ID 0906c00bb21d391ed7d0f64e9b0f5002193246d1
# Parent  a3f8c9f16d264687a1fac294cc2579fda1233c56
recode utf8 for ML, as done in feeder.pl;

diff -r a3f8c9f16d26 -r 0906c00bb21d lib/scripts/recode.pl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/recode.pl	Thu Aug 01 22:20:07 2013 +0200
@@ -0,0 +1,12 @@
+#
+# Author: Makarius
+#
+# recode.pl - recode utf8 for ML
+#
+
+for (@ARGV) {
+  utf8::upgrade($_);
+  s/([\x80-\xff])/\\${\(ord($1))}/g;
+  print $_, " ";
+}
+
diff -r a3f8c9f16d26 -r 0906c00bb21d lib/scripts/run-polyml-5.5.1
--- a/lib/scripts/run-polyml-5.5.1	Thu Aug 01 22:19:32 2013 +0200
+++ b/lib/scripts/run-polyml-5.5.1	Thu Aug 01 22:20:07 2013 +0200
@@ -64,7 +64,8 @@
 MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
 
 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
-  "$POLY" -q -i $ML_OPTIONS --eval "$MLTEXT" --error-exit </dev/null
+  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+    --error-exit </dev/null
   RC="$?"
 else
   if [ -z "$TERMINATE" ]; then