-
Herbert Valerio Riedel authored
First attempt via 7a2c9dde wasn't working properly. This attempt should work better as it doesn't cause the makefile recipe to fail which causes `make` to emit additional varying output.
add6a303
First attempt via 7a2c9dde wasn't working properly. This attempt should work better as it doesn't cause the makefile recipe to fail which causes `make` to emit additional varying output.