diff options
| author | Ben10do <Ben10do@users.noreply.github.com> | 2017-06-10 18:21:38 +0100 |
|---|---|---|
| committer | Ben10do <Ben10do@users.noreply.github.com> | 2017-06-10 18:21:38 +0100 |
| commit | fc300ab0ee63a1ecbcead67c3a7019a0bfe8deb5 (patch) | |
| tree | d2f8eb76b30d94217696a890d2159f91132cc5ca /engine | |
| parent | 848b3ba3ecbf110c168b4f37292bccdc6e3f2531 (diff) | |
Fix parallelisation issues in Makefile
Introduces a minor hack, in order to ensure that the tools are built before the Makefile attempts to use any of the tools, even when using ‘make -j’.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions