]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/scripts/makeit
split into two major parts:
[helm.git] / helm / scripts / makeit
index afad01f3cff825f4eef11e5e2a255cf1c34aad63..64553523e67789a47b17043c3ff6c38005cbf619 100755 (executable)
@@ -1,11 +1,10 @@
 #!/bin/sh
 
-if test $# != 3; then
-       echo "Usage: makeit <version> <where> <to>"
+if test $# != 1; then
+       echo "Usage: makeit <from>"
        echo
-       echo "       <version> must be V7_mowgli"
-       echo "       <from/to> is either phd or marcello"
+  echo "<from> is the machine we connect from"
        exit 1
 fi
        
-sed -e "s/@COQV@/$1/" -e "s/@WHERE@/$2/" -e "s/@FROM@/$3/"
+sed -e "s/@FROM@/$1/"