aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorpboutill2011-04-08 16:26:16 +0000
committerpboutill2011-04-08 16:26:16 +0000
commitc229186019d23d9893a12c5aae9a0f128f013a3d (patch)
tree8cfc3f353ec8abe521da9c29328194da307b2674 /scripts
parent27aa815d451fc21469019137399287196d9a187b (diff)
A kind of reply to bug 2444
coq_makefile uses ocaml{c,opt}.opt if it uses coqc -opt and ocaml‘c,opt} if it uses coqc -byte. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13980 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions