Closed maroneze closed 1 year ago
Add verbose option to avoid displaying dozens of Line #! /bin/sh skipped when running headache on the Frama-C sources. The messages can still be enabled by adding -v to the command line.
Line #! /bin/sh skipped
-v
Add verbose option to avoid displaying dozens of
Line #! /bin/sh skippedwhen running headache on the Frama-C sources. The messages can still be enabled by adding-vto the command line.