aboutsummaryrefslogtreecommitdiff
path: root/sysinit
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-02-09 15:11:48 +0000
committerGitHub2021-02-09 15:11:48 +0000
commit0e70966f73e9298254ac5f2e52668f2ead6a0452 (patch)
tree41cb8e004ee5793c4d22d4526dc18e1facec2adc /sysinit
parent16765871394a81975047b37f15a902fcc112dc40 (diff)
parentf6a695c81f7833683e846dddce5d5156254eaa92 (diff)
Merge PR #13810: ide: shift+enter to find backwards
Reviewed-by: herbelin
Diffstat (limited to 'sysinit')
0 files changed, 0 insertions, 0 deletions