aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2015-03-13 19:46:37 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2015-03-13 19:46:37 +0000
commitaf4904017b6ba7b5ff180e581a8379010b6b66d0 (patch)
tree6240993219dc66ad50e01568728a6c69a882f6d1 /Makefile.devel
parentdbb555f8daa1ab6ae17479545ea7fd49a63341c0 (diff)
Summary: remove non-BSD cp arg
Diffstat (limited to 'Makefile.devel')
-rw-r--r--Makefile.devel4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.devel b/Makefile.devel
index a9325f7a..a201231b 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -134,7 +134,7 @@ CVS_RELEASENAME = Release-$(CVS_VERSION)
# Where to release (i.e. copy) a new distribution to.
# This may be the final directory (local) or temporary directory.
-# was: RELEASEDIR = /home/proofgen/www
+# # was: RELEASEDIR = /home/proofgen/www
RELEASEDIR = /tmp/proofgeneral-www
# How to make the release "live". (Could be "true" to do nothing).
@@ -412,7 +412,7 @@ release: check distclean tag dist
mkdir -p $(RELEASEDIR)
(cd $(DISTBUILDIR); rm -f $(NAME))
(cd $(RELEASEDIR); rm -rf $(RELEASENAME))
- cp -pfdR $(DISTBUILDIR)/* $(RELEASEDIR)
+ cp -pfR $(DISTBUILDIR)/* $(RELEASEDIR)
(cd $(RELEASEDIR); rm -f $(LATESTNAME); ln -s $(RELEASENAME) $(LATESTNAME))
(cd $(RELEASEDIR); ln -sf $(RELEASENAMETGZ) $(LATESTNAME).tgz)
(cd $(RELEASEDIR); echo $(PRERELEASE_TAG) > $(PREREL_TAG_FILE))