From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- extraction/extraction.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'extraction/extraction.v') diff --git a/extraction/extraction.v b/extraction/extraction.v index dc7522b8..fb6bd397 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -115,7 +115,7 @@ Extract Constant Compiler.time => "Timing.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) (* Cabs *) -Extract Constant Cabs.cabsloc => +Extract Constant Cabs.cabsloc => "{ lineno : int; filename: string; byteno: int; -- cgit