aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqwc.mll
diff options
context:
space:
mode:
authorGravatar Ralf Jung <post@ralfj.de>2018-03-20 20:13:59 +0100
committerGravatar Ralf Jung <post@ralfj.de>2018-03-20 20:13:59 +0100
commit93817b4c2b8d96d6eb990dcfaf21cf2e8f2375df (patch)
tree8b6a84c8a29c7071e3209130de5da9dfaf0ad08a /tools/coqwc.mll
parent17c94dca5fe2fc19137b9cac923d51e8eb818041 (diff)
coq_makefile: FLAG make variables should not contain LIBS
Diffstat (limited to 'tools/coqwc.mll')
0 files changed, 0 insertions, 0 deletions