Skip to content
GitLab
Explore
Sign in
add a 'make' command to the dune main module. Usage
Code
Review changes
Check out branch
Download
Patches
Plain diff
Andreas Dedner
requested to merge
feature/pymainAddMake
into
master
Sep 11, 2023
Overview
0
Commits
2
Pipelines
6
Changes
8
Expand
python -m dune make -j4 modulebase or python -m dune make -j12 all
Merge request reports
Loading