aboutsummaryrefslogtreecommitdiff
path: root/distrib/Makefile
diff options
context:
space:
mode:
authorherbelin2002-01-10 19:56:09 +0000
committerherbelin2002-01-10 19:56:09 +0000
commitabdfeedd0047ea94913b328d63d23989afd886ad (patch)
tree52fb261729e32ba29f9b7a04c20dcc0b48358284 /distrib/Makefile
parente44d076a1aaaebe28cf9c1252db47fa7b7ca97ba (diff)
Bugs et raffinements
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2390 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'distrib/Makefile')
-rw-r--r--distrib/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/distrib/Makefile b/distrib/Makefile
index be2b22451f..0563057a25 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -277,7 +277,7 @@ prep-ftp-install:
- mkdir $(FTPDIR)/V${VERSION}
- chmod g+w ${FTPDIR}/V${VERSION}
-final-ftp_install:
+final-ftp-install:
(cd $(FTPDIR); rm -f current;ln -sf V${VERSION} current)
tar-gz-ftp-install: prep-ftp-install