aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar mlasson <marc.lasson@gmail.com>2015-06-25 15:41:27 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-09-03 00:46:52 +0200
commit0f2d41755d99770c4576776462a4e433fb8f0a02 (patch)
tree1df5fbd0f37d559728482d676b1a5848bb09fcf5 /library/library.ml
parentae8f843303060e1db96f72b42d744b8b200b0968 (diff)
Missing argument "-c" for coqdep in coq_makefile
Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d were generated by a call to coqdep using the argument -c (for ocaml code). While doing some finetuning of the generation of implicit rules, this commit removed (I think by mistake) this "-c". And without this -c argument coqdep output nothing on mllib files leading to incorrect linking of mllibs.
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions