diff options
| author | Gaëtan Gilbert | 2018-10-16 16:45:13 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:28:58 +0100 |
| commit | e6c64a54f8f52ff555a0857a2909f5f70b22e591 (patch) | |
| tree | 8d986606f5ed977bcd57397de930d6f88ee322ee /doc/plugin_tutorial/Makefile | |
| parent | 58b9174b229863c694ad65984b86b112c689ae10 (diff) | |
Fix for coq/coq#8515 (command driven attributes)
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions