diff options
| author | Maxime Dénès | 2019-04-09 11:03:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-09 11:03:13 +0200 |
| commit | 5463cfbaaaab2e696c4bbeeeb38f03ca79d5949e (patch) | |
| tree | f5903e140972be1dfc5052fc74e51b9c21feb813 /doc/plugin_tutorial/tuto2/Makefile | |
| parent | d47892548aebfb6640a8721ee1ec3493bfd3ce2a (diff) | |
Adapt to Coq's PR #9909
Diffstat (limited to 'doc/plugin_tutorial/tuto2/Makefile')
0 files changed, 0 insertions, 0 deletions