A small but essential file...

diff --git a/Doc/tools/whichlibs b/Doc/tools/whichlibs
new file mode 100755 (executable)
index 0000000..b7efe14
--- /dev/null
+++ b/Doc/tools/whichlibs
@@ -0,0 +1,2 @@
+#! /bin/sh
+sed -n 's/^\\input{\(lib[a-zA-Z0-9_]*\)}.*/\1.tex/p' lib.tex

diff --git a/Doc/whichlibs b/Doc/whichlibs
new file mode 100755 (executable)
index 0000000..b7efe14
--- /dev/null
+++ b/Doc/whichlibs
@@ -0,0 +1,2 @@
+#! /bin/sh
+sed -n 's/^\\input{\(lib[a-zA-Z0-9_]*\)}.*/\1.tex/p' lib.tex