/lib/Tools/
drwxr-xr-x [up]
-rwxr-xr-x 2000-03-24 08:56 +0100 732 browser
-rwxr-xr-x 2000-03-24 08:56 +0100 699 doc
-rwxr-xr-x 2000-03-24 08:56 +0100 1966 document
-rwxr-xr-x 2000-03-24 08:56 +0100 765 expandshort
-rwxr-xr-x 2000-03-24 08:56 +0100 515 findlogics
-rwxr-xr-x 2000-03-24 08:56 +0100 604 fixclasimp
-rwxr-xr-x 2000-03-24 08:56 +0100 639 fixdatatype
-rwxr-xr-x 2000-03-24 08:56 +0100 666 fixdots
-rwxr-xr-x 2000-03-24 08:56 +0100 615 fixgoal
-rwxr-xr-x 2000-03-24 08:56 +0100 614 fixseq
-rwxr-xr-x 2000-03-24 08:56 +0100 884 getenv
-rwxr-xr-x 2000-03-24 08:56 +0100 2547 install
-rwxr-xr-x 2000-03-24 08:56 +0100 655 installfonts
-rwxr-xr-x 2000-03-24 08:56 +0100 1906 latex
-rwxr-xr-x 2000-03-24 08:56 +0100 1212 logo
-rwxr-xr-x 2000-03-24 08:56 +0100 365 make
-rwxr-xr-x 2000-03-24 08:56 +0100 652 makeall
-rwxr-xr-x 2000-03-24 08:56 +0100 3476 mkdir
-rwxr-xr-x 2000-03-24 08:56 +0100 561 nonascii
-rwxr-xr-x 2000-03-24 08:56 +0100 179 symbolinput
-rwxr-xr-x 2000-03-24 08:56 +0100 3585 usedir