diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-02 11:17:54 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-02 11:17:54 +0200 |
| commit | 0057815355ae6a276028e5997e6fe841e41c3983 (patch) | |
| tree | dfa96374d7826f17bc9277b0dd05dff4e05a44bc /.github | |
| parent | a9b4d88ff0f403ea3503f1c5eedc4959ce4c2e30 (diff) | |
| parent | aa681a064cf15f3aeb55fde48dfe049d39e4065f (diff) | |
Merge PR #7370: Fix PHONY typo in coq_makefile
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions