diff options
Diffstat (limited to 'doc/tools/whichlibs')
| -rwxr-xr-x | doc/tools/whichlibs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/tools/whichlibs b/doc/tools/whichlibs new file mode 100755 index 0000000..10d44ee --- /dev/null +++ b/doc/tools/whichlibs @@ -0,0 +1,2 @@ +#!/bin/sh +sed -n 's%^\\input{\(lib[a-zA-Z0-9_]*\)}.*%../lib/\1.tex%p' ../lib/lib.tex |