diff options
Diffstat (limited to 'distrib/Makefile')
| -rw-r--r-- | distrib/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/distrib/Makefile b/distrib/Makefile index 16c4264b41..2ee5b8dd3e 100644 --- a/distrib/Makefile +++ b/distrib/Makefile @@ -436,11 +436,11 @@ tar-gz-ftp-install: prep-ftp-install src-rpm-ftp-install: prep-ftp-install chmod g+w $(COQSRCRPM) - $(CP) $(COQSRCRPM) $(FTPVDIR)/ + $(CP) *.src.rpm $(FTPVDIR)/ arch-rpm-ftp-install: prep-ftp-install chmod g+w $(COQRPM) - $(CP) $(COQRPM) $(FTPVDIR)/ + $(CP) *.$(ARCH).rpm $(FTPVDIR)/ arch-tar-gz-ftp-install: prep-ftp-install chmod g+w $(ARCHTARGZ) |