aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-01-21 14:42:29 +0100
committerPierre-Marie Pédrot2021-01-22 12:51:35 +0100
commit14875457711853bcbf7021fba9490e554324a043 (patch)
tree977860436cfeefba148f5c30e206e84cdb0fc682 /plugins
parent56e2c0391dda94b80fab8c8993ea17ea5d807797 (diff)
Add documentation for Ltac2 Printf.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions