diff options
| author | coqbot | 2020-08-05 12:42:46 +0200 |
|---|---|---|
| committer | GitHub | 2020-08-05 12:42:46 +0200 |
| commit | 51ecccef0308eceec1ddd9776a03fd993b3ea71a (patch) | |
| tree | 8abc156947ca86046dcd824e55998b68f0a79ca3 /Makefile.dev | |
| parent | 40b4e84b78745506aa9b173fb5c08e7ea74faaaa (diff) | |
| parent | 54ba930765c78df111d60d2cb60b95f9869344df (diff) | |
Merge PR #12724: CI metacoq: make .merlin
Reviewed-by: Zimmi48
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions