diff options
| author | Makarius Wenzel | 2006-02-12 13:47:18 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2006-02-12 13:47:18 +0000 |
| commit | a33a90a4d91df59c51ee51061157ae11209507ee (patch) | |
| tree | 9d5dc8e17c35fd0be85345b30a0ee58bf8e8d0c9 /generic | |
| parent | 9ea00d485050d4ed13e2a7e034eb918dfd63de33 (diff) | |
isar-preprocessing: replace \n by \<^newline>;
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions