diff options
| author | Gaëtan Gilbert | 2019-02-13 13:22:24 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 14:43:36 +0100 |
| commit | 0a465063a5501d9a84088fff8b1c8a62f63feec3 (patch) | |
| tree | c3408be3830a2815a302de0fcb004db3c1941bfb /plugins | |
| parent | f8d6c322783577b31cf55f8b55568ac56104202b (diff) | |
Add diff rule for README.rst to dune refman-html alias
We change regen_readme such that when given an argument it outputs
there instead of overwriting the readme.
Prompted by me noticing I forgot to regen in #9553.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions