| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-08-18 | Avoid running configure when plugins/ modified | Gaƫ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. | |||
