diff options
author | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 14:12:22 +0200 |
---|---|---|
committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 14:12:22 +0200 |
commit | 5aafa1d18ac4e5c4f61e046faae7b862781ce31d (patch) | |
tree | 1e014c1d5ae6e4d62cb43b2a1f1c52d854ec6634 /tactics/hipattern.mli | |
parent | 7037e774a0dacbf9335e7fde03ac6932e434343d (diff) |
User queries can be terminated with "...".
This appends the currently selected word to the query. Only queries
that end with this are supported, "..." inside the query will just
not work.
Diffstat (limited to 'tactics/hipattern.mli')
0 files changed, 0 insertions, 0 deletions