diff options
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 |