From: Stephane Glondu Date: Fri, 24 Jul 2020 14:17:11 +0000 (+0200) Subject: Refresh patches X-Git-Tag: archive/raspbian/4.08.1-10+rpi1^2~20 X-Git-Url: https://dgit.raspbian.org/?a=commitdiff_plain;h=1de5369128cdb03558bf92230c6d18a523d3dc7e;p=ocaml.git Refresh patches --- diff --git a/debian/patches/0006-read_main_debug_info-do-not-die-in-custom-executable.patch b/debian/patches/0006-read_main_debug_info-do-not-die-in-custom-executable.patch index 8239d571..586ddbe6 100644 --- a/debian/patches/0006-read_main_debug_info-do-not-die-in-custom-executable.patch +++ b/debian/patches/0006-read_main_debug_info-do-not-die-in-custom-executable.patch @@ -5,7 +5,6 @@ Subject: read_main_debug_info: do not die in -custom executables This fatal error occurred with some executables linked with -custom (with the Debian-specific patch), notably ppx preprocessors during the build of ppxlib. - --- runtime/backtrace_byt.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-)