aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-02-07 11:56:19 +0100
committerGaëtan Gilbert2019-02-12 14:39:49 +0100
commite5fb9c5cbce5e7e7e8fcb3d82c45074f9c165158 (patch)
treec769ba01f6e235f8ec021a2531477e6eda9d6290 /dev
parentd32a0db7b4d0775820b306badfe8072bd74cf62d (diff)
Fix failing coqtops in micromega.rst (the main one requires csdp)
Maybe we should still let it run but let's disable it until we install csdp on the build server at least.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions