aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/plugin_base.dune
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-04-03 12:00:28 +0200
committerPierre-Marie Pédrot2020-04-09 13:35:52 +0200
commitf0741920c339b219b5c80b9cd721bebec6028e20 (patch)
treef30f86f8cadb7cd86f4a78ec641437ece0d372ce /plugins/funind/plugin_base.dune
parent97939fdb603fe41c26a99a501fffa8b10bd07bbe (diff)
Code simplification in find_projectable_vars.
We inline the "with_evars := false" case.
Diffstat (limited to 'plugins/funind/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions