Fri, 21 May 1999 11:40:34 +0200 | wenzelm | history commands; | changeset | files |
Fri, 21 May 1999 11:40:15 +0200 | wenzelm | tuned; | changeset | files |
Fri, 21 May 1999 11:39:47 +0200 | wenzelm | adapted to History changes; | changeset | files |
Fri, 21 May 1999 11:38:57 +0200 | wenzelm | local_qed: obtain interactive flag; | changeset | files |
Fri, 21 May 1999 11:38:23 +0200 | wenzelm | backup replaced by checkpoint; | changeset | files |
Fri, 21 May 1999 11:37:36 +0200 | wenzelm | added default_prompt; | changeset | files |
Fri, 21 May 1999 11:36:56 +0200 | wenzelm | optional limit; | changeset | files |