diff options
| author | Emilio Jesus Gallego Arias | 2020-06-05 17:31:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-05 17:31:36 +0200 |
| commit | de430532053269a53661b923161d693ab11950b6 (patch) | |
| tree | 137e2d5e1d56013e7b03866bb31f97389aacbfb5 /dev | |
| parent | 0379ab63a3a84bae6da8b8d5ae42af4261520279 (diff) | |
| parent | 2b337fa8eb06fd1b3c1b8d783a88d59289dd56c9 (diff) | |
Merge PR #12456: Fix version switcher when building with Dune.
Reviewed-by: ejgallego
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions