diff options
| author | Pierre-Marie Pédrot | 2017-10-07 22:46:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-07 22:46:45 +0200 |
| commit | f0fb8686377815978556e7d554f27de6406d1fed (patch) | |
| tree | 84cd4552bb3329ce1808fb467622b602b87dd892 /doc/plugin_tutorial/tuto2 | |
| parent | 78832226d6e472a6592dfffe91242613ec76841c (diff) | |
Fix coq/ltac2#30: Compilation broken since -safe-string PR got merged.
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions