diff options
| author | Théo Zimmermann | 2020-06-05 17:09:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-05 17:09:33 +0200 |
| commit | 2b337fa8eb06fd1b3c1b8d783a88d59289dd56c9 (patch) | |
| tree | 5bd43b699901fa78f241856e5c84e9089b3f2332 /dev | |
| parent | 4f4ad5678db3e7aaf42f14d6d2d9000550c5f826 (diff) | |
Adjust list of versions in version switcher.
- Use the name 'dev' instead of 'master' because it is less cryptic.
- Add the 'v8.12' branch.
- Use the branch version only for active branches, and the latest
patch-level release for the rest.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions