summaryrefslogtreecommitdiff
path: root/debian/patches
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 15:41:29 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 15:41:29 +0200
commit38db629f4be6f0a963b95a958a99bbe382b6b5d1 (patch)
tree24ad74ded15f1bfd4744360f0151c0df3b5367fb /debian/patches
parent1950fa2f34bb93fe514e9035284073221c1cbba6 (diff)
Remove browser.dpatch and use --browser configure option
Diffstat (limited to 'debian/patches')
-rw-r--r--debian/patches/00list1
-rwxr-xr-xdebian/patches/browser.dpatch19
2 files changed, 0 insertions, 20 deletions
diff --git a/debian/patches/00list b/debian/patches/00list
index 96c8fc3a..a86c4963 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1,3 +1,2 @@
-browser
no-complexity-test
check
diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch
deleted file mode 100755
index 15647950..00000000
--- a/debian/patches/browser.dpatch
+++ /dev/null
@@ -1,19 +0,0 @@
-#! /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 &"