aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ide
diff options
context:
space:
mode:
authorGravatar Jim Fehrle <jfehrle@sbcglobal.net>2018-06-28 13:04:27 -0700
committerGravatar Jim Fehrle <jfehrle@sbcglobal.net>2018-06-30 10:21:21 -0700
commit069d17f4f138fd779eff589119a7783784ababd9 (patch)
tree0a7fb0841703b7273f4609f3a0744e452239b78b /Makefile.ide
parent74640d2b8bc158b301c0646db19747a86313e25a (diff)
Rebuild coqtop$(EXE) in "make coqbinaries" in addition to coqtop.opt$(EXE).
Fixes #7758.
Diffstat (limited to 'Makefile.ide')
0 files changed, 0 insertions, 0 deletions