diff options
| author | Clément Pit-Claudel | 2019-05-10 09:47:02 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-12 22:00:08 -0400 |
| commit | a101fdc131bd5d7a8ed1470cd7fa705ad6979e92 (patch) | |
| tree | 1ef4b6e2518e3b3d2b9d521830d6c5fbf8cf6aac /doc/sphinx/_static/notations.css | |
| parent | 57ed5dbda3241eef38ebff11196bc38ca9fa3f05 (diff) | |
[refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug'
Diffstat (limited to 'doc/sphinx/_static/notations.css')
0 files changed, 0 insertions, 0 deletions