aboutsummaryrefslogtreecommitdiff
path: root/Makefile.vofiles
AgeCommit message (Expand)Author
2019-11-01[make] install .vos along with .voEnrico Tassi
2019-05-07Fix PLUGINSVO computation after ltac2 integrationGaëtan Gilbert
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
2019-02-06Makefiles: Fixes for byte compilationGaëtan Gilbert
2019-01-10[make] support for QUICKEnrico Tassi
2018-05-30Makefile: fix undefined NATIVEFILES when -native-compute noGaëtan Gilbert
2018-05-23Don't try to install native compiled files if native-compile is not setJim Fehrle
2018-05-16Modify make system to include Makefile.common in the test suiteGaëtan Gilbert