/lib/Tools/
drwxr-xr-x [up]
-rwxr-xr-x 2000-09-11 18:00 +0200 863 browser
-rwxr-xr-x 2000-09-11 18:00 +0200 883 doc
-rwxr-xr-x 2000-09-11 18:00 +0200 2163 document
-rwxr-xr-x 2000-09-11 18:00 +0200 856 expandshort
-rwxr-xr-x 2000-09-11 18:00 +0200 653 findlogics
-rwxr-xr-x 2000-09-11 18:00 +0200 695 fixclasimp
-rwxr-xr-x 2000-09-11 18:00 +0200 730 fixdatatype
-rwxr-xr-x 2000-09-11 18:00 +0200 757 fixdots
-rwxr-xr-x 2000-09-11 18:00 +0200 706 fixgoal
-rwxr-xr-x 2000-09-11 18:00 +0200 705 fixseq
-rwxr-xr-x 2000-09-11 18:00 +0200 971 getenv
-rwxr-xr-x 2000-09-11 18:00 +0200 2671 install
-rwxr-xr-x 2000-09-11 18:00 +0200 740 installfonts
-rwxr-xr-x 2000-09-11 18:00 +0200 2423 latex
-rwxr-xr-x 2000-09-11 18:00 +0200 1309 logo
-rwxr-xr-x 2000-09-11 18:00 +0200 448 make
-rwxr-xr-x 2000-09-11 18:00 +0200 743 makeall
-rwxr-xr-x 2000-09-11 18:00 +0200 3697 mkdir
-rwxr-xr-x 2000-09-11 18:00 +0200 650 nonascii
-rwxr-xr-x 2000-09-11 18:00 +0200 264 symbolinput
-rwxr-xr-x 2000-09-11 18:00 +0200 3411 usedir