aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMaxime Dénès2018-11-27 08:49:45 +0100
committerMaxime Dénès2018-12-12 12:25:52 +0100
commitce0924599497800773ebc95b392e678926ea1820 (patch)
treeebb84815c8d88c282b3f554fd8ff91b5382c7125 /dev
parent84a950c8e1fa06d0dd764e9a426edbd987a7989e (diff)
User flags for coqtop/coqc in Makefile and CI build template
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions