aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/impargs.ml
diff options
context:
space:
mode:
authorGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2016-06-02 14:12:22 +0200
committerGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2016-06-02 14:12:22 +0200
commit5aafa1d18ac4e5c4f61e046faae7b862781ce31d (patch)
tree1e014c1d5ae6e4d62cb43b2a1f1c52d854ec6634 /library/impargs.ml
parent7037e774a0dacbf9335e7fde03ac6932e434343d (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 'library/impargs.ml')
0 files changed, 0 insertions, 0 deletions