]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/scripts/makeit
Error message updated.
[helm.git] / helm / scripts / makeit
index bbd7cfd05ae757551bb6caa500a9c2cff809df3f..afad01f3cff825f4eef11e5e2a255cf1c34aad63 100755 (executable)
@@ -3,7 +3,7 @@
 if test $# != 3; then
        echo "Usage: makeit <version> <where> <to>"
        echo
-       echo "       <version> is either V6.2 or V7"
+       echo "       <version> must be V7_mowgli"
        echo "       <from/to> is either phd or marcello"
        exit 1
 fi