diff options
| author | Théo Zimmermann | 2018-12-19 10:13:05 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-19 10:13:05 +0100 |
| commit | 41400286140d8808412b697642d92df063cb3464 (patch) | |
| tree | 71180f6c93211ff87cb62fa8a65735e1c617570e /dev/tools/github-check-prs.py | |
| parent | 2cad4dec40cef2aecb19c5a0e5a1368392be8d88 (diff) | |
| parent | fed7e17aa4345f02129a9a595abb1abd29f4d510 (diff) | |
Merge PR #9081: [dune] A new Makefile.dune target for each package (coq, coqide-server and coqide).
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions