From aced54ff681f671b2c5b99d18dddbbc570ac2a57 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Tue, 2 Jul 2024 15:19:41 +0200 Subject: [PATCH] ada: Accept duplicate SPARK_Mode pragmas in configuration files For consistency, we now accept duplicate SPARK_Mode pragmas in configuration files just like we accept other duplicate pragas there. gcc/ada/ * sem_prag.adb (Analyze_Pragma): Don't check for duplicate SPARK_Mode pragmas in configuration files. --- gcc/ada/sem_prag.adb | 8 -------- 1 file changed, 8 deletions(-) diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 52d63cf4492..e41fb2f8618 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -24758,14 +24758,6 @@ package body Sem_Prag is if No (Context) then Check_Valid_Configuration_Pragma; - - if Present (SPARK_Mode_Pragma) then - Duplication_Error - (Prag => N, - Prev => SPARK_Mode_Pragma); - raise Pragma_Exit; - end if; - Set_SPARK_Context; -- The pragma acts as a configuration pragma in a compilation unit -- 2.47.3