lib/scripts/recode.pl
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 52835 0906c00bb21d
child 62506 860cd901ab43
permissions -rw-r--r--
updated for release;
wenzelm@52835
     1
#
wenzelm@52835
     2
# Author: Makarius
wenzelm@52835
     3
#
wenzelm@52835
     4
# recode.pl - recode utf8 for ML
wenzelm@52835
     5
#
wenzelm@52835
     6
wenzelm@52835
     7
for (@ARGV) {
wenzelm@52835
     8
  utf8::upgrade($_);
wenzelm@52835
     9
  s/([\x80-\xff])/\\${\(ord($1))}/g;
wenzelm@52835
    10
  print $_, " ";
wenzelm@52835
    11
}
wenzelm@52835
    12