rwxr-xr-x 4273/0      0 Jun 17 16:51 1994 extras/
rw-r--r-- 4273/0   3972 Jun 17 14:31 1994 extras/Installation
rwxr-xr-x 4273/0      0 Jun 17 14:31 1994 extras/further-domains/
rw-r--r-- 4273/0 2580611 Jun 17 14:32 1994 extras/userguide.ps
rw-r--r-- 4273/0  85697 Jun 17 14:31 1994 extras/mobal.ps