aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
authorClément Pit-Claudel2019-05-20 17:32:59 -0400
committerClément Pit-Claudel2020-03-19 13:51:06 -0400
commit9492db6eeab7c8d29d7f4374fdbafe659149b231 (patch)
treeaa529bb7780895e3b1722ccd21a7396f02bbf151 /dev/doc
parent918e301faa228190f885f860510f4b6c352620f5 (diff)
[refman] Remove workaround for sphinx-doc/sphinx#4983
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions