diff options
| author | Théo Zimmermann | 2020-03-22 13:14:33 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-24 11:22:45 +0100 |
| commit | 9252e89072239c8c1454e754f8498031dfacec54 (patch) | |
| tree | 62eba55646f12a2e21312787adcf6bb93270afdd /dev/tools/pre-commit | |
| parent | c7d56372c7a2fff283fc4841f29cb0d5893aa431 (diff) | |
Fix world and watch targets of Makefile.dune now that doc has install rules.
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions