summaryrefslogtreecommitdiff
path: root/src/Makefile-non-opam
AgeCommit message (Expand)Author
2017-02-03fix headersPeter Sewell
2014-10-08Merge.Stephen Kell
2014-10-08Tweak Makefile to use absolute or relative paths consistently, fixing make be...Stephen Kell
2014-10-06Getting closer with non-opam makefileKathy Gray
2014-10-04Add alternative non-opam Makefile in src/.Stephen Kell