diff --git a/Doc/tools/whichlibs b/Doc/tools/whichlibs
new file mode 100755
index 00000000000..b7efe14d1c0
--- /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
index 00000000000..b7efe14d1c0
--- /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