diff options
| author | Clément Pit--Claudel | 2015-02-16 12:20:56 -0500 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-07-27 14:21:32 +0200 |
| commit | 05f22a5d6d5b8e3e80f1a37321708ce401834430 (patch) | |
| tree | c332b75a4817c15caa55e238a009311486c57432 /kernel/nativelambda.mli | |
| parent | 1674b11594a7b4daf24d99a0acdffc54c9999198 (diff) | |
search: Add an output-name-only search option
When set, search results only display symbol names, instead of
displaying full terms with types. This is useful when the list of
symbols is needed by an external program, in particular for doing
completion in IDEs.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions