From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- exportclight/Clightgen.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'exportclight/Clightgen.ml') diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index c1009b4f..5e8d77a7 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -75,7 +75,7 @@ let print_error oc msg = let output_filename ?(final = false) source_file source_suffix output_suffix = match !option_o with | Some file when final -> file - | _ -> + | _ -> Filename.basename (Filename.chop_suffix source_file source_suffix) ^ output_suffix @@ -253,7 +253,7 @@ let cmdline_actions = Exact "-dparse", Set option_dparse; Exact "-dc", Set option_dcmedium; Exact "-dclight", Set option_dclight; -(* General options *) +(* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); ] -- cgit