Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
authorwenzelm
Wed, 03 Nov 2010 21:53:56 +0100
changeset 40335 3e4bb6e7c3ca
parent 40334 69930308b896
child 40336 755862729f8d
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
lib/scripts/feeder file | annotate | diff | comparison | revisions
lib/scripts/feeder.pl file | annotate | diff | comparison | revisions 
--- a/lib/scripts/feeder	Wed Nov 03 17:11:40 2010 +0100
+++ b/lib/scripts/feeder	Wed Nov 03 21:53:56 2010 +0100
@@ -16,7 +16,7 @@
   echo "Usage: $PRG [OPTIONS]"
   echo
   echo "  Options are:"
-  echo "    -h TEXT      head text"
+  echo "    -h TEXT      head text (encoded as utf8)"
   echo "    -p           emit my pid"
   echo "    -q           do not pipe stdin"
   echo "    -t TEXT      tail text"
--- a/lib/scripts/feeder.pl	Wed Nov 03 17:11:40 2010 +0100
+++ b/lib/scripts/feeder.pl	Wed Nov 03 21:53:56 2010 +0100
@@ -24,7 +24,11 @@
 
 $emitpid && (print $$, "\n");
 
-$head && (print "$head", "\n");
+if ($head) {
+  utf8::encode($head);
+  $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
+  print $head, "\n";
+}
 
 if (!$quit) {
   while (<STDIN>) {
isabelle