diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-12-07 14:21:35 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-12-07 14:21:35 +0100 |
| commit | a4410595a448c9b5b44cfd75e2c2f48e664d5aea (patch) | |
| tree | 28f62efe550c94baf36c0f8d2786823e26ff430d /hol-light | |
| parent | 4a4a8c5e3ce8b5db1e893ac9c800f76a2c29d124 (diff) | |
Speeding up indentation.
Dedicated regexp for bullets when searching backward.
Diffstat (limited to 'hol-light')
0 files changed, 0 insertions, 0 deletions