1 files changed, 21 insertions, 0 deletions
diff --git a/manual/texis.awk b/manual/texis.awk
new file mode 100644
index 0000000000..a2a8dbfe09
--- /dev/null
+++ b/manual/texis.awk
@@ -0,0 +1,21 @@
+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[stackptr]);
+	}
+    }
+    print "";
+}