/lib/scripts/
drwxr-xr-x [up]
-rw-r--r-- 2010-02-02 09:48 +0000 2735 dimacs2hol.pl
-rwxr-xr-x 2010-02-02 09:48 +0000 1013 feeder
-rw-r--r-- 2010-02-02 09:48 +0000 450 feeder.pl
-rwxr-xr-x 2010-02-02 09:48 +0000 231 fileident
-rw-r--r-- 2010-02-02 09:48 +0000 2812 getsettings
-rw-r--r-- 2010-02-02 09:48 +0000 2471 keywords.pl
-rwxr-xr-x 2010-02-02 09:48 +0000 1203 polyml-platform
-rwxr-xr-x 2010-02-02 09:48 +0000 369 polyml-version
-rwxr-xr-x 2010-02-02 09:48 +0000 1218 run-mosml
-rwxr-xr-x 2010-02-02 09:48 +0000 1963 run-polyml
-rwxr-xr-x 2010-02-02 09:48 +0000 2019 run-polyml-5.0
-rwxr-xr-x 2010-02-02 09:48 +0000 1808 run-smlnj
-rw-r--r-- 2010-02-02 09:48 +0000 470 system.pl
-rw-r--r-- 2010-02-02 09:48 +0000 432 timestart.bash
-rw-r--r-- 2010-02-02 09:48 +0000 1387 timestop.bash
-rw-r--r-- 2010-02-02 09:48 +0000 1394 unsymbolize.pl
-rw-r--r-- 2010-02-02 09:48 +0000 539 yxml.pl