Wed, 31 Aug 2005 15:46:48 +0200 | wenzelm | added line break for 'uses'; | changeset | files |
Wed, 31 Aug 2005 15:46:47 +0200 | wenzelm | added no_body_context; | changeset | files |
Wed, 31 Aug 2005 15:46:46 +0200 | wenzelm | use_dir: added copy-dump option; | changeset | files |
Wed, 31 Aug 2005 15:46:45 +0200 | wenzelm | present_text: Toplevel.no_body_context prevents use of wrong context in interaction; | changeset | files |