obsolete;

--- a/lib/scripts/recode.pl	Wed Mar 09 20:44:02 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-#
-# Author: Makarius
-#
-# recode.pl - recode utf8 for ML
-#
-
-for (@ARGV) {
-  utf8::upgrade($_);
-  s/([\x80-\xff])/\\${\(ord($1))}/g;
-  print $_;
-}