summaryrefslogtreecommitdiff
path: root/Makefile.best_binaries
Commit message (Expand)AuthorAgeFilesLines
* nicer style in Makefile.best_binariesXavier Leroy2019-10-121-24/+17
* Makefile.best_binaries: only use the native tool when it is newer (not stale)Gabriel Scherer2019-10-121-17/+24
* Makefile.best_binaries: best-effort commands for OCAML{C,OPT,DEP,LEX}Gabriel Scherer2019-10-121-0/+46