diff options
Diffstat (limited to 'manual/texis.awk')
| -rw-r--r-- | manual/texis.awk | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/manual/texis.awk b/manual/texis.awk deleted file mode 100644 index 153724755d..0000000000 --- a/manual/texis.awk +++ /dev/null @@ -1,21 +0,0 @@ -BEGIN { - print "texis = \\"; - for(x = 1; x < ARGC; x++) - { - input[0] = ARGV[x]; - print ARGV[x], "\\"; - for (s = 0; s >= 0; s--) - { - while ((getline < input[s]) > 0) - { - if ($1 == "@include") - { - input[++s] = $2; - print $2, "\\"; - } - } - close(input[s]); - } - } - print ""; -} |