diff options
| author | Hendrik Tews | 2020-10-31 13:10:28 +0100 |
|---|---|---|
| committer | hendriktews | 2020-12-19 16:43:49 +0100 |
| commit | e90af80638d5e367f5e7f9d8e0af5dd9028e2377 (patch) | |
| tree | a22724d18e9ee1aa25357fc5f11c8b4a5ca217f3 /acl2 | |
| parent | 9064f143b7aae41cfcbfcf5270ab69a81887f21f (diff) | |
redesign of parallel background compilation without clones
- no clones any more, existing jobs are directly linked
- the whole require command is processed by coqdep to determine
the required files, this fixes #352
- the require commands are a separate kind of jobs, because they
do not need to get compiled
- queue items are only stored in require jobs and file jobs can
not have a queue dependency, this simplifies the logic
Diffstat (limited to 'acl2')
0 files changed, 0 insertions, 0 deletions
