]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/toglie_helm_xref.sh
Initial revision
[helm.git] / helm / interface / toglie_helm_xref.sh
diff --git a/helm/interface/toglie_helm_xref.sh b/helm/interface/toglie_helm_xref.sh
new file mode 100755 (executable)
index 0000000..b3cb4e0
--- /dev/null
@@ -0,0 +1,5 @@
+#!/bin/bash
+
+echo "****" $1
+cp $1 /tmp/pippo
+cat /tmp/pippo | ./toglie_helm_xref.pl > $1