aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/_static
diff options
context:
space:
mode:
authorClément Pit-Claudel2019-05-10 09:47:02 -0400
committerClément Pit-Claudel2019-05-12 22:00:08 -0400
commita101fdc131bd5d7a8ed1470cd7fa705ad6979e92 (patch)
tree1ef4b6e2518e3b3d2b9d521830d6c5fbf8cf6aac /doc/sphinx/_static
parent57ed5dbda3241eef38ebff11196bc38ca9fa3f05 (diff)
[refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug'
Diffstat (limited to 'doc/sphinx/_static')
0 files changed, 0 insertions, 0 deletions