From a3b1c98ecfe89edb297cf3fbf525120343d63f1d Mon Sep 17 00:00:00 2001
From: Tristan Gingold <tgingold@free.fr>
Date: Sat, 21 Nov 2020 08:54:35 +0100
Subject: Ignore plusargs options (that starts with a '+').  For #1517

---
 src/grt/grt-options.adb | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/grt')

diff --git a/src/grt/grt-options.adb b/src/grt/grt-options.adb
index eadca0068..d3d7a260e 100644
--- a/src/grt/grt-options.adb
+++ b/src/grt/grt-options.adb
@@ -239,6 +239,9 @@ package body Grt.Options is
       Status := Decode_Option_Ok;
       if Option = "--" then
          Status := Decode_Option_Last;
+      elsif Option (1) = '+' then
+         --  For VPI/VHPI - plusargs.
+         null;
       elsif Option = "--help" or else Option = "-h" then
          Help;
          Status := Decode_Option_Stop;
-- 
cgit v1.2.3