Fix installation stage
What does this MR do?
Few things make the installation stage fail when performing
make install. Here some fixes for them.
When installing DORiE (i.e.
make install), many header files are wrong while many others are missing. That makes installation to fail. This MR fixes that and installation now is at least successful.
Installation of python dune virtual environment is currently activated by default. This is alright for using the build files but is incorrect for proper installations. This MR fixes that. If the user still wants to install with editable mode, she/he can set the corresponding dune flag for it.
Changes after discussions
The CLI can now handle executing DORiE from install directory trees. This is controlled via the
The application docker image now uses the DORiE install tree instead of the build tree to reduce image size, see also #44.
Is there something that needs to be double checked?
Does installation work with
Can this MR be accepted?
[ ] Added/Updated testsSee #201
[ ] Added/Updated documentationSee #201
- Pipeline passing
- Squash option set
- Delete branch option set
Added entry to
Assignee: If the Squash option is set, check/update the commit message right before merging!