Sat, 16 Jul 2011 18:41:35 +0200 | wenzelm | some file and directory operations; | changeset | files |
Sat, 16 Jul 2011 18:20:02 +0200 | wenzelm | more general bash_process, which allows to terminate background processes as well; | changeset | files |
Sat, 16 Jul 2011 18:11:14 +0200 | wenzelm | updated to Poly/ML SVN 1328, which is considered 5.4.2; | changeset | files |