/lib/Tools/
drwxr-xr-x [up]
-rwxr-xr-x 2001-11-14 23:22 +0100 1406 browser
-rwxr-xr-x 2001-11-14 23:22 +0100 892 convert
-rwxr-xr-x 2001-11-14 23:22 +0100 893 doc
-rwxr-xr-x 2001-11-14 23:22 +0100 2131 document
-rwxr-xr-x 2001-11-14 23:22 +0100 866 expandshort
-rwxr-xr-x 2001-11-14 23:22 +0100 661 findlogics
-rwxr-xr-x 2001-11-14 23:22 +0100 705 fixclasimp
-rwxr-xr-x 2001-11-14 23:22 +0100 740 fixdatatype
-rwxr-xr-x 2001-11-14 23:22 +0100 767 fixdots
-rwxr-xr-x 2001-11-14 23:22 +0100 716 fixgoal
-rwxr-xr-x 2001-11-14 23:22 +0100 715 fixseq
-rwxr-xr-x 2001-11-14 23:22 +0100 735 fixsome
-rwxr-xr-x 2001-11-14 23:22 +0100 981 getenv
-rwxr-xr-x 2001-11-14 23:22 +0100 3324 install
-rwxr-xr-x 2001-11-14 23:22 +0100 1288 installfonts
-rwxr-xr-x 2001-11-14 23:22 +0100 2436 latex
-rwxr-xr-x 2001-11-14 23:22 +0100 1319 logo
-rwxr-xr-x 2001-11-14 23:22 +0100 458 make
-rwxr-xr-x 2001-11-14 23:22 +0100 738 makeall
-rwxr-xr-x 2001-11-14 23:22 +0100 5256 mkdir
-rwxr-xr-x 2001-11-14 23:22 +0100 660 nonascii
-rwxr-xr-x 2001-11-14 23:22 +0100 272 symbolinput
-rwxr-xr-x 2001-11-14 23:22 +0100 855 unsymbolize
-rwxr-xr-x 2001-11-14 23:22 +0100 4434 usedir