| Sun, 31 May 2009 17:47:04 +0200 | wenzelm | eliminated misleading dummy versions of print/makestring, cf. 6974449ddea9; | changeset | files |
| Sun, 31 May 2009 17:45:53 +0200 | wenzelm | provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources; | changeset | files |
| Sun, 31 May 2009 16:41:52 +0200 | wenzelm | no longer open PolyML -- to avoid surprises within the global name space; | changeset | files |