/lib/scripts/
drwxr-xr-x [up]
-rw-r--r-- 2000-01-17 14:10 +0100 1850 expandshort.pl
-rwxr-xr-x 2000-01-17 14:10 +0100 1102 feeder
-rw-r--r-- 2000-01-17 14:10 +0100 2813 feeder.pl
-rw-r--r-- 2000-01-17 14:10 +0100 938 fixclasimp.pl
-rw-r--r-- 2000-01-17 14:10 +0100 1220 fixdatatype.pl
-rw-r--r-- 2000-01-17 14:10 +0100 1313 fixdots.pl
-rw-r--r-- 2000-01-17 14:10 +0100 875 fixgoal.pl
-rw-r--r-- 2000-01-17 14:10 +0100 1324 fixseq.pl
-rw-r--r-- 2000-01-17 14:10 +0100 932 getsettings
-rwxr-xr-x 2000-01-17 14:10 +0100 1364 isa-emacs
-rwxr-xr-x 2000-01-17 14:10 +0100 2467 isa-xterm
-rw-r--r-- 2000-01-17 14:10 +0100 1034 patch-scripts.bash
-rwxr-xr-x 2000-01-17 14:10 +0100 1209 run-mlworks
-rwxr-xr-x 2000-01-17 14:10 +0100 1762 run-polyml
-rwxr-xr-x 2000-01-17 14:10 +0100 1792 run-smlnj
-rwxr-xr-x 2000-01-17 14:10 +0100 1560 run-smlnj-0.93
-rwxr-xr-x 2000-01-17 14:10 +0100 245 showtime
-rw-r--r-- 2000-01-17 14:10 +0100 2485 symbolinput.pl