diff options
Diffstat (limited to 'doc/makefile')
| -rw-r--r-- | doc/makefile | 24 | 
1 files changed, 24 insertions, 0 deletions
| diff --git a/doc/makefile b/doc/makefile new file mode 100644 index 0000000..1d3bb63 --- /dev/null +++ b/doc/makefile @@ -0,0 +1,24 @@ +# Copyright (C) 2010, 2020 Jose Antonio Ortega Ruiz +# +# This file is free software; as a special exception the author gives +# unlimited permission to copy and/or distribute it, with or without +# modifications, as long as this notice is preserved. +# +# This program is distributed in the hope that it will be useful, but +# WITHOUT ANY WARRANTY, to the extent permitted by law; without even the +# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + +top_srcdir=.. +output_dir=html + +web: +	rm -f $(output_dir)/*.html +	texi2html --output=$(output_dir) \ +                  --split=chapter \ +                  --noheader \ +                  --nonumber-section \ +                  --init-file=$(top_srcdir)/doc/site.conf \ +                  --top-file=index.html \ +                  $(top_srcdir)/doc/web.texi +	cp $(top_srcdir)/doc/geiser.css ${output_dir} +	cp -r $(top_srcdir)/doc/img ${output_dir} | 
