Commit 09f630849f5a9cc540b1289cdd7a034b171fa7d4

Stefan Sperling 2020-03-20T15:33:01

use one consistent way to compute the Git URL to write to the config file