diff options
Diffstat (limited to 'asis.gpr-patch')
| -rw-r--r-- | asis.gpr-patch | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/asis.gpr-patch b/asis.gpr-patch new file mode 100644 index 000000000000..8535dd0515d4 --- /dev/null +++ b/asis.gpr-patch @@ -0,0 +1,11 @@ +--- 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 + + |