Currently if an unrecognized warning is passed to CompCert, the compiler will error out. Clang will print a warning (they have a -Wunknown-warning-option) and continue compilation. I’d like to request consideration for following the same behavior as clang. This would make it easier to plug CompCert into existing build systems via “env CC=ccomp make” without having to retrofit gcc/clang build systems very much. To illustrate the difference in behavior, compare:

cc -Wunrecognized

vs.

ccomp -Wunrecognized