/lib/Tools/
drwxr-xr-x [up]
-rwxr-xr-x 2004-06-12 22:44 +0200 1381 browser
-rwxr-xr-x 2004-06-12 22:44 +0200 892 convert
-rwxr-xr-x 2004-06-12 22:44 +0200 893 doc
-rwxr-xr-x 2004-06-12 22:44 +0200 2259 document
-rwxr-xr-x 2004-06-12 22:44 +0200 866 expandshort
-rwxr-xr-x 2004-06-12 22:44 +0200 661 findlogics
-rwxr-xr-x 2004-06-12 22:44 +0200 705 fixclasimp
-rwxr-xr-x 2004-06-12 22:44 +0200 740 fixdatatype
-rwxr-xr-x 2004-06-12 22:44 +0200 767 fixdots
-rwxr-xr-x 2004-06-12 22:44 +0200 716 fixgoal
-rwxr-xr-x 2004-06-12 22:44 +0200 893 fixgreek
-rwxr-xr-x 2004-06-12 22:44 +0200 715 fixseq
-rwxr-xr-x 2004-06-12 22:44 +0200 735 fixsome
-rwxr-xr-x 2004-06-12 22:44 +0200 981 getenv
-rwxr-xr-x 2004-06-12 22:44 +0200 3324 install
-rwxr-xr-x 2004-06-12 22:44 +0200 2835 latex
-rwxr-xr-x 2004-06-12 22:44 +0200 1319 logo
-rwxr-xr-x 2004-06-12 22:44 +0200 458 make
-rwxr-xr-x 2004-06-12 22:44 +0200 866 makeall
-rwxr-xr-x 2004-06-12 22:44 +0200 6194 mkdir
-rwxr-xr-x 2004-06-12 22:44 +0200 855 unsymbolize
-rwxr-xr-x 2004-06-12 22:44 +0200 4436 usedir
-rwxr-xr-x 2004-06-12 22:44 +0200 222 version