diff options
| author |  Samuel Mimram <smimram@debian.org> | 2007-04-09 15:19:11 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2007-04-09 15:19:11 +0000 |
| commit | cb73a339553ac8a5449b3bf850207ed7500ff147 (patch) | |
| tree | 7d40fc574e70c01211d07d84e9276cc7d814dd5d /debian/patches/browser.dpatch | |
| parent | 9636b0c333690f13552f68e38a76fc070cf14762 (diff) | |
Uploading to unstable.debian/8.1+dfsg-3
Diffstat (limited to 'debian/patches/browser.dpatch')
| -rwxr-xr-x | debian/patches/browser.dpatch | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch new file mode 100755 index 00000000..ba55f3de --- /dev/null +++ b/debian/patches/browser.dpatch @@ -0,0 +1,19 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## browser.dpatch by Samuel Mimram <smimram@debian.org> +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Use the default Debian browser for help. + +@DPATCH@ +diff -urNad coq-8.0pl3+8.1alpha~/lib/options.ml coq-8.0pl3+8.1alpha/lib/options.ml +--- coq-8.0pl3+8.1alpha~/lib/options.ml 2005-12-26 20:07:21.000000000 +0000 ++++ coq-8.0pl3+8.1alpha/lib/options.ml 2006-04-29 16:06:20.000000000 +0000 +@@ -117,7 +117,4 @@ + "\" must contain exactly one placeholder \"%s\".") + else pre,post + with +- Not_found -> +- if Sys.os_type = "Win32" +- then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", "" +- else "netscape -remote \"OpenURL(", ")\"" ++ Not_found -> "/usr/bin/x-www-browser ", "" |