| changeset 10096 | 6cbe69107c18 |
| parent 10091 | 43c1951a369c |
| child 11239 | be12c6f1ea75 |
--- a/Admin/page/Makefile Wed Sep 27 19:37:32 2000 +0200 +++ b/Admin/page/Makefile Wed Sep 27 19:39:50 2000 +0200 @@ -38,9 +38,6 @@ # --- begin rules all: clean main dist install weblint - @echo "###" - @echo "### Finished. See main/ and dist/ for the resulting pages." - @echo "###" main: @$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)