diff options
Diffstat (limited to 'debian/patches/no-external-doc-resources.patch')
| -rw-r--r-- | debian/patches/no-external-doc-resources.patch | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/debian/patches/no-external-doc-resources.patch b/debian/patches/no-external-doc-resources.patch index df35669d..735ac63b 100644 --- a/debian/patches/no-external-doc-resources.patch +++ b/debian/patches/no-external-doc-resources.patch @@ -1,5 +1,15 @@ +From: Gard Spreemann <gspreemann@gmail.com> +Date: Fri, 18 May 2018 19:09:11 +0200 +Subject: no-external-doc-resources + Remove external resource references from Doxygen header. Later upstream versions will include an alternative header that does the job. +--- + doc/common/header.html | 60 -------------------------------------------------- + 1 file changed, 60 deletions(-) + +diff --git a/doc/common/header.html b/doc/common/header.html +index 9c51438..6a02a89 100644 --- a/doc/common/header.html +++ b/doc/common/header.html @@ -8,8 +8,6 @@ @@ -11,7 +21,7 @@ versions will include an alternative header that does the job. <!-- GUDHI website css for header END --> <link href="$relpath^tabs.css" rel="stylesheet" type="text/css"/> <script type="text/javascript" src="$relpath^jquery.js"></script> -@@ -22,64 +20,6 @@ +@@ -22,64 +20,6 @@ $extrastylesheet </head> <body> |