From 1de5369128cdb03558bf92230c6d18a523d3dc7e Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Jul 2020 16:17:11 +0200 Subject: [PATCH] Refresh patches --- ...06-read_main_debug_info-do-not-die-in-custom-executable.patch | 1 - 1 file changed, 1 deletion(-) 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(-) -- 2.30.2