diff options
| author | Makarius Wenzel | 2009-08-28 20:30:40 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2009-08-28 20:30:40 +0000 |
| commit | 795c8bdebac6f356bf810e5ac06a6c1addc8f9f5 (patch) | |
| tree | 88f15196282698315951dcda4668e7d588622336 /generic | |
| parent | 1f6baad655836ad24047cb1caac63b2d0384a5da (diff) | |
isar-nonwrap-regexp: ML should work (note that there are *many* ML commands);
added separate isar-string-wrapping;
isar-positions-of: isar-string-wrapping of file name -- to make double sure;
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions