]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/scripts/makeit
Removed stuff no longer in use.
[helm.git] / helm / scripts / makeit
diff --git a/helm/scripts/makeit b/helm/scripts/makeit
deleted file mode 100755 (executable)
index 6455352..0000000
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/bin/sh
-
-if test $# != 1; then
-       echo "Usage: makeit <from>"
-       echo
-  echo "<from> is the machine we connect from"
-       exit 1
-fi
-       
-sed -e "s/@FROM@/$1/"