diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2024-07-02 15:19:41 +0200 |
|---|---|---|
| committer | Marc Poulhiès <dkm@gcc.gnu.org> | 2024-08-01 17:14:38 +0200 |
| commit | aced54ff681f671b2c5b99d18dddbbc570ac2a57 (patch) | |
| tree | 231eee1d61dc76821a35780caed3c83b5fc43b51 /gcc/ada | |
| parent | 54d6ce3f067f529e2dbfe237a12e5b65548e298c (diff) | |
| download | gcc-aced54ff681f671b2c5b99d18dddbbc570ac2a57.zip gcc-aced54ff681f671b2c5b99d18dddbbc570ac2a57.tar.gz gcc-aced54ff681f671b2c5b99d18dddbbc570ac2a57.tar.bz2 | |
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.
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/sem_prag.adb | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 52d63cf..e41fb2f 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 |