]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/toglie_helm_xref.sh
This commit was manufactured by cvs2svn to create branch 'init'.
[helm.git] / helm / interface / toglie_helm_xref.sh
diff --git a/helm/interface/toglie_helm_xref.sh b/helm/interface/toglie_helm_xref.sh
deleted file mode 100755 (executable)
index b3cb4e0..0000000
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/bin/bash
-
-echo "****" $1
-cp $1 /tmp/pippo
-cat /tmp/pippo | ./toglie_helm_xref.pl > $1