diff options
Diffstat (limited to 'asis.gpr-patch')
| -rw-r--r-- | asis.gpr-patch | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/asis.gpr-patch b/asis.gpr-patch deleted file mode 100644 index 8535dd0515d4..000000000000 --- a/asis.gpr-patch +++ /dev/null @@ -1,11 +0,0 @@ ---- asis-gpl-2017-src/asis.gpr -+++ asis-gpl-2017-src-new/asis.gpr -@@ -22,6 +22,7 @@ - ------------------------------------------------------------------------------ - - with "common"; -+with "gnat_util"; - - project Asis is - - |