aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
diff options
context:
space:
mode:
authorLysxia2019-07-27 09:11:02 -0400
committerLysxia2019-07-27 09:11:02 -0400
commitb5fc7e9e8efc18935d562bd0690c9667fdc8066f (patch)
treeae2ac34343e6421e7a9632c9ae39e4c7d952d008 /dev/ci/ci-basic-overlay.sh
parent2e37b4b30d0779dc960db80189e51ecd69f7e45a (diff)
[coqdoc] Nest <a> into <h2> instead of the other way around
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions