aboutsummaryrefslogtreecommitdiff
path: root/lib/objFile.ml
diff options
context:
space:
mode:
authorEnrico Tassi2020-11-24 19:31:56 +0100
committerEnrico Tassi2020-11-26 12:06:25 +0100
commitfdf2f92ed5e2e838ffb11183c00f724e4e7c3a51 (patch)
treea174d17652b2cd2d1080afae0088c4c8b6423f3b /lib/objFile.ml
parent66370041661beb850c20d53d43111674a32d84b2 (diff)
[ci] separate oddorder and fourcolor from mathcomp
In this way interval does not have to wait too much
Diffstat (limited to 'lib/objFile.ml')
0 files changed, 0 insertions, 0 deletions