diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index b26c3d0487045d078e9aaab35946321d12bdba7c..d029891d4a2bffbfac1b22fa016f7ca188765a2e 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -523,12 +523,12 @@ let build_cpp_cmd = function let exe = cpp_name cmdl in let clang_no_warn = if exe = "clang" || exe = "gcc" then - (* NB: For gcc only old versions (still found in Ubuntu 18.04, + (* NB: For gcc, only old versions (still found in Ubuntu 18.04, supported until 2028, though) activate builtin-macro-redefined. This is also the case for newer clangs, while older ones will complain about the unknown warning (gcc does not seem to care, so that it is safe to keep the unknown-warning-option in every - case. *) + case). *) ["-Wno-builtin-macro-redefined"; "-Wno-unknown-warning-option"] else []