aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/algebra
diff options
context:
space:
mode:
authorYves Bertot2019-11-20 15:34:31 +0100
committerMaxime Dénès2019-11-25 16:23:14 +0100
commit054024e3b03eeb2f4ce93a904d68bcc4f216d38b (patch)
tree6d0ed0f250a1995a9254734d1af8c14a4cd10508 /mathcomp/algebra
parentc08f721483b7d6e8da64f8f475ce68bbaff5b05c (diff)
things that are needed to make 'make doc' work
Diffstat (limited to 'mathcomp/algebra')
0 files changed, 0 insertions, 0 deletions