/lib/Tools/
drwxr-xr-x [up]
-rwxr-xr-x 1998-08-27 20:46 +0200 350 browser
-rwxr-xr-x 1998-08-27 20:46 +0200 689 doc
-rwxr-xr-x 1998-08-27 20:46 +0200 719 expandshort
-rwxr-xr-x 1998-08-27 20:46 +0200 515 findlogics
-rwxr-xr-x 1998-08-27 20:46 +0200 564 fixclasimp
-rwxr-xr-x 1998-08-27 20:46 +0200 599 fixdatatype
-rwxr-xr-x 1998-08-27 20:46 +0200 626 fixdots
-rwxr-xr-x 1998-08-27 20:46 +0200 575 fixgoal
-rwxr-xr-x 1998-08-27 20:46 +0200 574 fixseq
-rwxr-xr-x 1998-08-27 20:46 +0200 884 getenv
-rwxr-xr-x 1998-08-27 20:46 +0200 849 install
-rwxr-xr-x 1998-08-27 20:46 +0200 655 installfonts
-rwxr-xr-x 1998-08-27 20:46 +0200 362 make
-rwxr-xr-x 1998-08-27 20:46 +0200 618 makeall
-rwxr-xr-x 1998-08-27 20:46 +0200 521 nonascii
-rwxr-xr-x 1998-08-27 20:46 +0200 139 symbolinput
-rwxr-xr-x 1998-08-27 20:46 +0200 3069 usedir