aboutsummaryrefslogtreecommitdiff
path: root/API/API.mllib
diff options
context:
space:
mode:
authorJason Gross2017-10-13 13:27:06 -0400
committerJason Gross2017-10-13 13:27:06 -0400
commit43e3768ae50a1a4ab3dbb77cdd46b3a810f31453 (patch)
tree40bbe122e7c42a18946064ff6303770ea18d7faa /API/API.mllib
parentf8975f9fce08c7d43e6e57be980cfa36635969a9 (diff)
Fix BZ#5785 (make install -j broken)
This adds back `$(MKDIR) $(FULLCOQLIB)/toploop`, which was lost between 8.6 and 8.7.
Diffstat (limited to 'API/API.mllib')
0 files changed, 0 insertions, 0 deletions