diff options
| author | Pierre-Marie Pédrot | 2016-08-28 23:02:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-29 14:05:40 +0200 |
| commit | aa0ad1713b109da690f9a56358df1f5ba56c65e6 (patch) | |
| tree | dbf5ce24a603443d7e5f8dc52843a863ae68370f /dev/base_include | |
| parent | f2fb98eabdb2f550c177609ad70ab8ba57821bca (diff) | |
Fix inefficiency in CoqIDE display of tagged text.
The helper code in LablGTK is algorithmically slow, so that
we rather reimplement it as a small helper function.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions