diff options
| author | Clément Pit-Claudel | 2018-05-18 01:10:15 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-06-19 10:58:37 +0200 |
| commit | 3d8342c2c26f710583e6b9246bd1069cb8b42d7d (patch) | |
| tree | 9bb701aa5a231ed02a3c899052399f78717f56b5 /dev/ci | |
| parent | 21a0af5b7743e5a1013438210492991b51d878c4 (diff) | |
[doc] Rewrite and document the prodn directive
It was broken and undocumented. We dropped the git logs, too, so it wasn't clear
who wrote it and why it was introduced in the first place.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions