aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar Clément Pit-Claudel <clement.pitclaudel@live.com>2018-05-18 01:12:10 -0400
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-19 10:58:37 +0200
commit36e38a3768251dbcf20c4de2b746e5eee33da909 (patch)
tree6a2dcb6260bc856a320f7db435902983eb031873 /config
parent981864d47efca1d42f43dc5b7c5439638a86f315 (diff)
[doc] Use productionlist instead of prodn in ring.rst
Diffstat (limited to 'config')
0 files changed, 0 insertions, 0 deletions