From 12231700b0122295b97aae6ad3e268d2eb0a6361 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 2 Jun 2023 14:30:31 +0000
Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s)
---
src/kernel_services/ast_queries/file.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index b26c3d04870..d029891d4a2 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
[]
--
GitLab