Vadim Zeitlin 84b1b3f8b5 Do not use "make -s" in the CI builds ... We want to have as much information as possible in case of the build failure, so don't use the "--silent" make option.		2021-09-30 17:29:38 +02:00
..
workflows	Do not use "make -s" in the CI builds	2021-09-30 17:29:38 +02:00