-
Lorenz Huedepohl authored
Apparently, this is now necessary when compiling in another directory than the top-level
e30aeb43
On Thursday, 2nd February from 9 to 10.00 am there will be a maintenance with a short downtime of the GitLab service.
Apparently, this is now necessary when compiling in another directory than the top-level