aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGuillaume Melquiond2019-11-07 16:27:16 +0100
committerGuillaume Melquiond2019-11-07 16:27:16 +0100
commit5b8a2855f719f42d81dd9ac3e8c5737fa8c7b2db (patch)
treead1580a3cc20413b78f68f11c49eb0748eb73d39 /dev
parent5c5831e35747f25d8aeadf10a13cd60e9b7adfbb (diff)
Do not include final stops in queries. (Fixes #11058)
The bug was introduced by #10063, which eagerly added dots to identifier without considering whether they are related to the identifier. Along the way, this commit also prevents primes and digits from being added as initial characters of identifiers. This works for both word selection and queries. Note that there is still a small issue with word selection, when the current word starts with a digit. Indeed, when double-clicking, GTK will already have extended the selection to it, so we have no way of preventing the digit from being part of the selection. This commit also fixes the unusual calling convention of Gtk_parsing.end_words.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions