aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-10-26 11:05:27 +0000
committerGitHub2020-10-26 11:05:27 +0000
commit9e7b0f9f248a1fae8e5681815bd621f182696c4f (patch)
tree8de9102f30e1e9d2161d6a43e098ed9985e3a7d3 /plugins/syntax
parent689e86b9241411180248e3115364a972833f0851 (diff)
parenta2ce4da4c2b0dc81d4c61f3e672d6c9d65dba46b (diff)
Merge PR #13257: adjust Search deprecation warning
Reviewed-by: Zimmi48 Reviewed-by: Blaisorblade
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions