diff options
| author | coqbot-app[bot] | 2020-09-21 12:41:39 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-21 12:41:39 +0000 |
| commit | 84d5475169ec0ba3d11928dab11eba6bc3d19d9b (patch) | |
| tree | aca44c92c1934839a16f36e49002d557474a0373 /dev/ci | |
| parent | fff4fe1120c81ab7b543cfb8d175cc4458e3c12e (diff) | |
| parent | cbb2efcaecff4e066d8ac37bd049a8e917bec9d6 (diff) | |
Merge PR #12723: dune: pass -bin-annot to configure
Reviewed-by: ejgallego
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions