| Sat, 06 Feb 2010 16:32:34 +0100 | wenzelm | removed unused "boundary" of Table/Graph.get_first; | changeset | files |
| Sat, 06 Feb 2010 15:51:22 +0100 | wenzelm | proper treatment of paths passed to the shell -- to allow spaces in file names as usual; | changeset | files |
| Sat, 06 Feb 2010 14:50:55 +0100 | wenzelm | renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh; | changeset | files |
| Sat, 06 Feb 2010 14:39:33 +0100 | wenzelm | misc tuning; | changeset | files |
| Sat, 06 Feb 2010 08:42:37 +0100 | haftmann | merged | changeset | files |
| Sat, 06 Feb 2010 08:42:22 +0100 | haftmann | adjusted to changeset 118b41bba42b5 | changeset | files |
| Sat, 06 Feb 2010 00:22:01 +0100 | wenzelm | tuned font handling; | changeset | files |