aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/plugin_base.dune
diff options
context:
space:
mode:
authorVincent Laporte2019-05-03 13:41:47 +0000
committerVincent Laporte2019-05-03 13:41:47 +0000
commita37d1c0e433f34d0ab5357b1f78eb0e04d961dc8 (patch)
treed986ebd93114b8b29711e8afc1811683905d4812 /plugins/syntax/plugin_base.dune
parent6960da4736186fa6214854329f36f558e7aa4d0b (diff)
parent24c570834dccc90c7ff14d3f6b9d33b818fa79c9 (diff)
Merge PR #10025: Fix #9994: `revert dependent` is extremely slow.
Ack-by: ppedrot Reviewed-by: vbgl
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions