diff options
| author | Pierre Roux | 2019-01-27 16:01:31 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-04-04 23:44:00 +0200 |
| commit | 0d8a4ec0f7486f47b7cff4cda465e2bd10c163ac (patch) | |
| tree | 8834c79b4efe2f2ccb516828956349ec2cb89f7d /doc/plugin_tutorial/tuto2/Makefile | |
| parent | dc903c82c2308ae638147c5428511abe9279bf6d (diff) | |
Adapt to coq/coq#8764
Diffstat (limited to 'doc/plugin_tutorial/tuto2/Makefile')
0 files changed, 0 insertions, 0 deletions