diff options
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..15647950 --- /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~/lib/flags.ml coq/lib/flags.ml +--- coq~/lib/flags.ml 2008-07-25 15:13:00.000000000 +0200 ++++ coq/lib/flags.ml 2008-07-25 15:30:47.000000000 +0200 +@@ -126,7 +126,4 @@ + let coq_netscape_remote_var = "COQREMOTEBROWSER" in + Sys.getenv coq_netscape_remote_var + with +- Not_found -> +- if Sys.os_type = "Win32" +- then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s" +- else "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &" ++ Not_found -> "/usr/bin/x-www-browser %s &" |