From b6f60c6af69cf51da6b112586ada5a6fadaa996a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 19 Dec 2014 20:54:38 +0100 Subject: [PATCH] remove junk in makefile.push_doc --- Makefile | 4 ---- 1 file changed, 4 deletions(-) diff --git a/Makefile b/Makefile index dcd252c4..c397b0dd 100644 --- a/Makefile +++ b/Makefile @@ -54,10 +54,6 @@ examples: all push_doc: doc scp -r containers.docdir/* cedeela.fr:~/simon/root/software/containers/ - scp -r containers_string.docdir/* cedeela.fr:~/simon/root/software/containers/string/ - scp -r containers_advanced.docdir/* cedeela.fr:~/simon/root/software/containers/advanced - scp -r containers_misc.docdir/* cedeela.fr:~/simon/root/software/containers/misc/ - scp -r containers_lwt.docdir/* cedeela.fr:~/simon/root/software/containers/lwt/ DONTTEST=myocamlbuild.ml setup.ml $(wildcard src/**/*.cppo.*) QTESTABLE=$(filter-out $(DONTTEST), \