/lib/scripts/
drwxr-xr-x [up]
-rw-r--r-- 1999-01-24 11:33 +0100 1806 expandshort.pl
-rwxr-xr-x 1999-01-24 11:33 +0100 1102 feeder
-rw-r--r-- 1999-01-24 11:33 +0100 2809 feeder.pl
-rw-r--r-- 1999-01-24 11:33 +0100 938 fixclasimp.pl
-rw-r--r-- 1999-01-24 11:33 +0100 1220 fixdatatype.pl
-rw-r--r-- 1999-01-24 11:33 +0100 1313 fixdots.pl
-rw-r--r-- 1999-01-24 11:33 +0100 875 fixgoal.pl
-rw-r--r-- 1999-01-24 11:33 +0100 1324 fixseq.pl
-rw-r--r-- 1999-01-24 11:33 +0100 718 getsettings
-rwxr-xr-x 1999-01-24 11:33 +0100 1328 isa-emacs
-rwxr-xr-x 1999-01-24 11:33 +0100 2121 isa-xterm
-rw-r--r-- 1999-01-24 11:33 +0100 970 patch-scripts.bash
-rwxr-xr-x 1999-01-24 11:33 +0100 1209 run-mlworks
-rwxr-xr-x 1999-01-24 11:33 +0100 1762 run-polyml
-rwxr-xr-x 1999-01-24 11:33 +0100 1792 run-smlnj
-rwxr-xr-x 1999-01-24 11:33 +0100 1560 run-smlnj-0.93
-rwxr-xr-x 1999-01-24 11:33 +0100 245 showtime
-rw-r--r-- 1999-01-24 11:33 +0100 2481 symbolinput.pl