aboutsummaryrefslogtreecommitdiff
path: root/config/list_plugins.ml
AgeCommit message (Collapse)Author
2020-08-18Avoid running configure when plugins/ modifiedGaƫtan Gilbert
We use an indirection, producing the sorted list of subdirectories of plugins/, so that dune can recognize it hasn't changed and doesn't rerun configure. Since configure regenerates a timestamp this avoids recompiling the stdlib. Fix #12750.