aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2020-02-06 17:27:05 +0100
committerGitHub <noreply@github.com>2020-02-06 17:27:05 +0100
commitd5435a34169d92a96f1436128f3e90df7f4f9e9a (patch)
tree51d678b64420e87bebe713b9a4c1aa043fb13685 /debug
parent6950ac8fb096768cb3811ae7f89d0db080bf965a (diff)
downloadcompcert-kvx-d5435a34169d92a96f1436128f3e90df7f4f9e9a.tar.gz
compcert-kvx-d5435a34169d92a96f1436128f3e90df7f4f9e9a.zip
Compatibility with OCaml 4.10 (#214)
debug/DwarfPrinter.mli: unused functor parameter trigger warning 69, replace by non-dependent functor type. Makefile.extr: turn warning 69 (unused functor parameter) off for extracted code configure: accept OCaml versions above 4.09 configure: update messages for unsupported versions of OCaml and Coq
Diffstat (limited to 'debug')
-rw-r--r--debug/DwarfPrinter.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli
index e1e10601..78dc05fb 100644
--- a/debug/DwarfPrinter.mli
+++ b/debug/DwarfPrinter.mli
@@ -12,7 +12,7 @@
open DwarfTypes
-module DwarfPrinter: functor (Target: DWARF_TARGET) ->
+module DwarfPrinter: DWARF_TARGET ->
sig
val print_debug: out_channel -> debug_entries -> unit
end