diff options
| author | Enrico Tassi | 2013-12-27 19:19:24 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-05 16:55:58 +0100 |
| commit | 929f9de11b22612ee3809a37222e417250ccda4f (patch) | |
| tree | fde8fde029d7fc4c2d776ecf81941ac7ebc11405 /dev/base_include | |
| parent | d5e353ded3282b2cb2314e8ee59315e3d14c4ce1 (diff) | |
Disable GlobRef feedback (CoqIDE does nothing with them)
The original idea was to send not the kernel name, but the file/line
to that CoqIDE could make the text an hyperlink to the file, exactly
as coqdoc generated HTML.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions