| commit | b6e24631fa1fc841da22329c9159bba9e177f1b0 | |
| author | malc <clamky@hotmail.com> | |
| Wed, 14 Apr 2021 15:25:12 +0000 (14 18:25 +0300) | ||
| committer | malc <clamky@hotmail.com> | |
| Wed, 14 Apr 2021 15:25:12 +0000 (14 18:25 +0300) | ||
| tree | 38bc4f477e0b6e97a932feaf4f85b6a4b6d9bfaf | treesnapshot (tar.gz zip) |
| parent | 87f80f295891b19950558e4b7d0cb7254cf1de31 | commitdiff |
Change compilation strategy
Also add Makefile generation.
Interface files are handled more correctly.
NB. When all the .ml files have corresponding .mli one the generated
Makefile shows noticable speed gain when "-j N" is used.
Also add Makefile generation.
Interface files are handled more correctly.
NB. When all the .ml files have corresponding .mli one the generated
Makefile shows noticable speed gain when "-j N" is used.
| build.bash | diffblobblamehistory | |
| misc/build.txt | [deleted file] | blobblamehistory |