Skip to content

paths_dist.py should depends on gen_paths_dist.sh in Makefile

Should fix re-configuring paths problem when the same dist tree is used

Merge request reports