diff options
| author | Marcello Stanisci <marcello.stanisci@inria.fr> | 2017-05-17 13:58:50 +0200 |
|---|---|---|
| committer | Marcello Stanisci <marcello.stanisci@inria.fr> | 2017-05-17 17:03:36 +0200 |
| commit | b09104aecf53fe261e8502d4cb2b5c5774dae063 (patch) | |
| tree | 9632b4bdc41fb1720e320ebe1af294564c945ce4 /doc/manual/Makefile.am | |
| parent | 744d81b5acc5a9c729b6bef45499f97833e8b773 (diff) | |
manual gpl boilerplate + commands to compile the manual
Diffstat (limited to 'doc/manual/Makefile.am')
| -rw-r--r-- | doc/manual/Makefile.am | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/manual/Makefile.am b/doc/manual/Makefile.am new file mode 100644 index 00000000..bb306355 --- /dev/null +++ b/doc/manual/Makefile.am @@ -0,0 +1,10 @@ +all: manual.pdf manual.html + +manual.pdf: + texi2pdf manual.texi + +manual.html: + texi2html manual.texi + +info_TEXINFOS = manual.texi +manual_TEXINFOS = version.texi |