diff options
| author | Emilio Jesus Gallego Arias | 2016-03-03 16:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-03-03 17:07:45 +0100 |
| commit | a8962654c562349f24728613352ea76268227471 (patch) | |
| tree | 8fbafaafec6783164b6e1b3b07a467a22b538e0a /docs/javascripts | |
| parent | 42ae48695694641c67a86adb299e34f6c1366f4f (diff) | |
[search] Use msg_info to notify search results.
By default, the search command calls `Pp.msg` to print search results.
Unfortunately, this bypasses the `log_via_feedback` option and produces
not very nice results on feedback-depending IDES like JsCoq.
A proper fix would involve merging coq/coq#143 , and the upcoming search
cleanup, but this should do the trick for now.
I couldn't observe any problem with the usual testing.
Diffstat (limited to 'docs/javascripts')
0 files changed, 0 insertions, 0 deletions