diff options
Diffstat (limited to 'doc/Makefile-files')
| -rw-r--r-- | doc/Makefile-files | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/doc/Makefile-files b/doc/Makefile-files index 8c490b1..d2b8992 100644 --- a/doc/Makefile-files +++ b/doc/Makefile-files @@ -6,5 +6,16 @@ UPLOAD_FILES += doc/ndim-git-cheatsheet.txt UPLOAD_FILES += doc/.htaccess EXTRA_DIST += doc/.htaccess -UPLOAD_FILES += doc/HEADER.html doc/FOOTER.html -EXTRA_DIST += doc/HEADER.html doc/FOOTER.html +UPLOAD_FILES += doc/HEADER.html +EXTRA_DIST += doc/HEADER.html + +UPLOAD_FILES += doc/FOOTER.html +CLEANFILES += doc/FOOTER.html + +EXTRA_DIST += build-helpers/txt2html.sed + +doc/FOOTER.html: $(top_srcdir)/README $(top_srcdir)/build-helpers/txt2html.sed + mkdir -p doc + $(SED) -f "$(top_srcdir)/build-helpers/txt2html.sed" $(top_srcdir)/README > "doc/FOOTER.html.new" + test -s "doc/FOOTER.html.new" + mv -f "doc/FOOTER.html.new" "doc/FOOTER.html" |