fix CI (!3) · Merge requests · Lorenz Huedepohl / ftimings · GitLab

The source project of this merge request has been removed.

Meisam Farzalipour Tabriz requested to merge (removed):master into master Feb 26, 2020

It was more involved than I initially thought! But seems to be working now.