diff options
| author | Théo Zimmermann | 2019-05-08 20:50:36 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-08 20:50:36 +0200 |
| commit | 50a89e6882e319cf6107147b49d387dd41e81805 (patch) | |
| tree | fa70140d4824adb07a2ed70c6ed17de57e247b69 /dev | |
| parent | e30d52a3c724a71bf43b46416c09e4b6ef1d1f67 (diff) | |
Define a new `is_a_released_version` variable in configure.ml.
Use it to not include unreleased changes when building a released
version.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions