Wed, 14 Apr 2004 14:13:05 +0200 | kleing | use more symbols in HTML output | changeset | files |
Wed, 14 Apr 2004 13:28:46 +0200 | wenzelm | renamed have_thms to note_thms; | changeset | files |
Wed, 14 Apr 2004 13:26:27 +0200 | wenzelm | tuned; | changeset | files |
Wed, 14 Apr 2004 13:25:51 +0200 | wenzelm | proper handling of lines terminated by CRLF or CR; | changeset | files |
Wed, 14 Apr 2004 12:19:16 +0200 | schirmer | * raw control symbols are of the form \<^raw:...> now. | changeset | files |
Wed, 14 Apr 2004 11:44:57 +0200 | berghofe | Fixed bug in check_mode_clause. | changeset | files |