Patch | Description | Author | Forwarded | Bugs | Origin | Last update |
---|---|---|---|---|---|---|
gprinstall-no-artifacts.diff | remove Artifacts from gnatcoll.gpr Gprinstall has no option to skip artifacts or change their destination. It is not installed during indep builds. |
Nicolas Boulenguez <nicolas@debian.org> | not-needed | |||
doc_path.diff | Give GPS Debian path when registering documentation. | Nicolas Boulenguez <nicolas@debian.org> | not-needed |