blob: 66540f2e61e3944ba6a045cf3df6a3af8816a264 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
:
# questo script, eseguito in questa directory
# genera tutti i formati della documentazione gawk
# che si possono ricavare a partire
# da gawktexi.in, nella directory ./manual
#
# dapprima si prepara il file di input (gawk.texi)
#
awk -f sidebar.awk < gawktexi.in > gawk.texi
#
# poi si invoca lo script che genera i vari formati
#
./gendocs.sh gawk gawk
|
