add option to disable papi even if available (!67) · Merge requests · starpu / starpu · GitLab

Mentions légales du service

The source project of this merge request has been removed.

Merged LEANDRO NESI Lucas requested to merge (removed):papi_option into master Oct 20, 2022

Add option to disable papi even if available