diff options
| author | Makarius Wenzel | 1999-07-08 15:23:16 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-07-08 15:23:16 +0000 |
| commit | 28f5eb4cec4fd70a294ae0e5169edb99faa4439d (patch) | |
| tree | 011879186a64170892a8632d07ce484916493bfe /html | |
| parent | 3afd5d82c2bc8516d2d94d7e1f6bc63bd1d3e280 (diff) | |
isar-stack-to-indent: indent according to (current-column) of open cmd;
fixed isar-count-undos, isar-find-and-forget: proper handling of empty and diag commands;
Diffstat (limited to 'html')
0 files changed, 0 insertions, 0 deletions