diff options
| author | Emilio Jesus Gallego Arias | 2018-03-10 02:03:08 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-10 11:39:58 +0200 |
| commit | 78c3d736a6a1c74d9bc8317e15895a1a0fbab341 (patch) | |
| tree | 31f7eaad28d8880a4b97656f28501fa9359ba15f /kernel | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
[build] Build checker generated files using a make rule.
Currently, `configure.ml` does copy/link some files from `kernel` to
`checker` in an ad-hoc way. Instead, it is preferable to add a copy
rule to make and let it handle the dependencies properly.
This also fixes a dependency bug in Windows, as files wouldn't be
properly refreshed if `configure` was not run each time.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions