1 files changed, 13 insertions, 0 deletions
diff --git a/doc/it/genera_formati.sh b/doc/it/genera_formati.sh
new file mode 100755
index 00000000..66540f2e
--- /dev/null
+++ b/doc/it/genera_formati.sh
@@ -0,0 +1,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