Commit 1722ae1c authored Nov 25, 2022 by Jan Kiene

Merge branch 'use--j-flag-for-make-in-scripts' into 'main'

add -j to make_options in scripts

See merge request !292