diff options
| author | Pierre Courtieu | 2019-06-18 15:28:24 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2019-06-18 15:28:24 +0200 |
| commit | 2ada467c2c2964a605659714f2a267db2c915952 (patch) | |
| tree | 7d3fbf40a738f04e482a4117083431f37252aa41 /doc | |
| parent | cdc630c3d453fe0c1384e3faca268f9818828c26 (diff) | |
Remove pghelp spans when retracting.
Due to performance issue (probably an emacs bug) and given the
uselessness of the pghelp spans in retracted regions. We simply remove
these spans when retracting.
The question remains to remove them completely or to make them more
useful. company-coq currently disables them anyway.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions