| Fri, 27 Aug 2010 00:02:32 +0200 | wenzelm | eliminated old 'local' command; | changeset | files |
| Thu, 26 Aug 2010 21:04:22 +0200 | wenzelm | more uniform descriptions, which end up in the collective output of 'print_attributes' for example; | changeset | files |
| Thu, 26 Aug 2010 20:42:09 +0200 | wenzelm | Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order; | changeset | files |