diff options
| author | Erik Martin-Dorel | 2018-12-20 16:24:14 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2018-12-21 12:17:14 +0100 |
| commit | ab8aefdcff6cf02e8cfe51bd052242f9907c5e72 (patch) | |
| tree | 80adde7d489d86b9d69f1d9ae29ee527006ad996 /docs/htmldoc/index_variable_A.html | |
| parent | da5985eae6656be1bd30aee76c8d08dbc3a09c25 (diff) | |
Add hidden job .make-build to also test the Makefile build infra
* This job is only instantiated with coqorg/coq:latest
* Add the associated Dockerfile.make
Diffstat (limited to 'docs/htmldoc/index_variable_A.html')
0 files changed, 0 insertions, 0 deletions