diff options
| -rw-r--r-- | manual/texis.awk | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/manual/texis.awk b/manual/texis.awk index a2a8dbfe09..153724755d 100644 --- a/manual/texis.awk +++ b/manual/texis.awk @@ -8,13 +8,13 @@ BEGIN { { while ((getline < input[s]) > 0) { - if ($1 == "@include") + if ($1 == "@include") { input[++s] = $2; print $2, "\\"; } } - close(input[stackptr]); + close(input[s]); } } print ""; |