From: Piotr Trojanek <troja...@adacore.com> 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. Tested on x86_64-pc-linux-gnu, committed on master. --- 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.45.2