diff options
| author | Clément Pit-Claudel | 2020-04-27 12:08:05 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-04-27 12:08:05 -0400 |
| commit | 040550c09033308f6c76b5630ee47fd9fab94327 (patch) | |
| tree | 72fe469b2503d1d0c6d72996564a94eaff66e49a /dev/ci/ci-basic-overlay.sh | |
| parent | f9f47108598fa2dfe705a4a58956803a4918bc52 (diff) | |
| parent | d1735b4914c43a50ff5c8d8c048a89f50ae33c4d (diff) | |
Merge PR #12090: Remove documentation for Hide menu in CoqIDE (was removed in 8.5).
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions