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