A small but essential file...

1994-01-02 01:22:36 +00:00 · 1994-01-02 01:22:36 +00:00 · 36b4807621
parent 5fdeeeae2a
commit 36b4807621
2 changed files with 4 additions and 0 deletions
--- a/Doc/tools/whichlibs
+++ b/Doc/tools/whichlibs
@ -0,0 +1,2 @@
+#! /bin/sh
+sed -n 's/^\\input{\(lib[a-zA-Z0-9_]*\)}.*/\1.tex/p' lib.tex
--- a/Doc/whichlibs
+++ b/Doc/whichlibs
@ -0,0 +1,2 @@
+#! /bin/sh
+sed -n 's/^\\input{\(lib[a-zA-Z0-9_]*\)}.*/\1.tex/p' lib.tex