]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/scripts/Makefile
Removed stuff no longer in use.
[helm.git] / helm / scripts / Makefile
diff --git a/helm/scripts/Makefile b/helm/scripts/Makefile
deleted file mode 100644 (file)
index be6ba21..0000000
+++ /dev/null
@@ -1,16 +0,0 @@
-
-all: 
-       - chmod ug+w phd*rc
-       ./makeit phd <template.cshrc >phd_mowgli.cshrc
-       ./makeit phd <template.rc >phd_mowgli.rc
-       ./makeit marcello <template.cshrc >phd_marcello_mowgli.cshrc
-       ./makeit marcello <template.rc >phd_marcello_mowgli.rc
-       chmod a+x phd*rc
-       chmod ug-w phd*rc
-
-clean:
-       rm -f phd*rc
-
-cleanbak:
-       rm -f *~
-