[Pkg-ocaml-maint-commits] [SCM] janest-core packaging branch, experimental/master, updated. debian/107.01-5-23-g05147b6

[Lifeng Sun]

The following commit has been merged in the experimental/master branch:
commit 611212c23d3c8a4b7c8eda4089504b463c3ccf8c
Author: Lifeng Sun <lifongsun at gmail.com>
Date:   Fri Jul 26 08:43:11 2013 +0800

    Remove 0001-escape-special-characters-in-doc.patch.
    
    Appled by upstream.

diff --git a/debian/patches/0001-escape-special-characters-in-doc.patch b/debian/patches/0001-escape-special-characters-in-doc.patch
deleted file mode 100644
index 5a9433b..0000000
--- a/debian/patches/0001-escape-special-characters-in-doc.patch
+++ /dev/null
@@ -1,16 +0,0 @@
---- a/lib/command.mli
-+++ b/lib/command.mli
-@@ -288,11 +288,11 @@
- 
-       The [name] must not be surrounded by whitespace, if it is, an exn will be raised.
- 
--      If the [name] is surrounded by a special character pair (<>, {}, [] or (),) 
-+      If the [name] is surrounded by a special character pair (<>, \{\}, \[\] or (),) 
-       [name] will remain as-is, otherwise, [name] will be uppercased.
- 
-       In the situation where [name] is only prefixed or only suffixed by one of the
--      special character pairs, or different pairs are used, (e.g. "<ARG]") an exn will
-+      special character pairs, or different pairs are used, (e.g. "<ARG\]") an exn will
-       be raised.
- 
-       The (possibly transformed) [name] is mentioned in the generated help for the 
diff --git a/debian/patches/series b/debian/patches/series
deleted file mode 100644
index 52791de..0000000
--- a/debian/patches/series
+++ /dev/null
@@ -1 +0,0 @@
-0001-escape-special-characters-in-doc.patch

-- 
janest-core packaging