diff options
| author | Arnold D. Robbins <arnold@skeeve.com> | 2017-04-12 13:06:17 +0300 |
|---|---|---|
| committer | Arnold D. Robbins <arnold@skeeve.com> | 2017-04-12 13:06:17 +0300 |
| commit | 5b78c79a7172eaf4f63369f54b804f9365a00d4b (patch) | |
| tree | 3f57fb8c0b09e4378de6c78f9bd5bcc5f8c7404c /doc/it/compila_originale.sh | |
| parent | 31246324a2be2ace19fed10302241a7bb45df6b6 (diff) | |
| parent | caba861750571c86af1e80731f1a43dc96b47e95 (diff) | |
| download | egawk-5b78c79a7172eaf4f63369f54b804f9365a00d4b.tar.gz egawk-5b78c79a7172eaf4f63369f54b804f9365a00d4b.tar.bz2 egawk-5b78c79a7172eaf4f63369f54b804f9365a00d4b.zip | |
Merge branch 'master' into feature/fix-comments
Diffstat (limited to 'doc/it/compila_originale.sh')
| -rwxr-xr-x | doc/it/compila_originale.sh | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/doc/it/compila_originale.sh b/doc/it/compila_originale.sh new file mode 100755 index 00000000..06d53b93 --- /dev/null +++ b/doc/it/compila_originale.sh @@ -0,0 +1,16 @@ + +# +# builds the PDF version of the Gawk manual, +# in the current directory +# +echo "Building the pdf version of the gawk manual" +echo "in directory:" +pwd +echo "Beware, it can take a long time!" +if [ -f "gawktexi.in" ] +then + gawk -f sidebar.awk gawktexi.in >gawk.texi +fi +# just in case, drop previous Index +rm -f gawk.cps gawk.cp gawk.aux gawk.fn gawk.ky gawk.log gawk.pg +texi2pdf gawk.texi |