]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/latinize.pl
This commit was manufactured by cvs2svn to create branch 'helm'.
[helm.git] / helm / interface / latinize.pl
diff --git a/helm/interface/latinize.pl b/helm/interface/latinize.pl
deleted file mode 100755 (executable)
index 7fa6787..0000000
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/perl
-
-while(<STDIN>)
-{
-  s/&#8594;/->/g;
-  s/&#8658;/=>/g;
-  s/&#955;/\\/g;
-  s/&#928;/||/g;
-  print;
-}