From: Johannes Kanig <[email protected]>
When an FSF frontend crash happens under GNATprove_Mode, the bugbox
should point users to the SPARK repository instead of the GCC bug
tracker.
Keep the existing GCC bug-report instructions for other FSF tools.
gcc/ada/ChangeLog:
* comperr.adb (Compiler_Abort): Use the SPARK bug-report URL in
GNATprove mode only, and keep the GCC bug-report URL for other
FSF tools.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/comperr.adb | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/gcc/ada/comperr.adb b/gcc/ada/comperr.adb
index 5a7ba6f5d7c..2ae38a7b399 100644
--- a/gcc/ada/comperr.adb
+++ b/gcc/ada/comperr.adb
@@ -296,7 +296,17 @@ package body Comperr is
-- Otherwise we use the standard fixed text
else
- if Is_FSF_Version then
+ if Is_FSF_Version and then GNATprove_Mode then
+ Write_Str
+ ("| Please submit a bug report at the SPARK issue" &
+ " tracker:");
+ End_Line;
+
+ Write_Str
+ ("| https://github.com/AdaCore/spark2014 .");
+ End_Line;
+
+ elsif Is_FSF_Version then
Write_Str
("| Please submit a bug report; see" &
" https://gcc.gnu.org/bugs/ .");
--
2.53.0
