# HG changeset patch
# User wenzelm
# Date 1457553324 -3600
# Node ID 739a84403864c8c05d98d49654b491ab59e5613b
# Parent  7e2aa1d67dd8e7324f19ba6fbc3fcc7e166d9d20
obsolete;

diff -r 7e2aa1d67dd8 -r 739a84403864 lib/scripts/recode.pl
--- 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 $_;
-}