From 0a500b73fc9bd6c6752c7bf0079e2305d0040303 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 14 Oct 2016 14:19:40 +0200 Subject: Remove undocumented option. Bug 20193 --- cparser/Rename.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser/Rename.mli') diff --git a/cparser/Rename.mli b/cparser/Rename.mli index c4ef2228..818a51bc 100644 --- a/cparser/Rename.mli +++ b/cparser/Rename.mli @@ -13,4 +13,4 @@ (* *) (* *********************************************************************) -val program : C.program -> string -> C.program +val program : C.program -> C.program -- cgit