diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index f825e1abdab4a930b7814d8f040410fbf0fae61e..76162715fd65fae908f99e2d5715ab2e3869d9fb 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -398,12 +398,13 @@ let build_cpp_cmd cmdl supp_args in_file out_file = and out_file = Filename.quote out_file in let substitute s = match Str.matched_string s with + | "%%" -> "%" | "%args" -> supp_args | "%1" | "%i" | "%input" -> in_file | "%2" | "%o" | "%output" -> out_file | s -> s (* Unrocognized parameters are left intact *) in - let regexp = Str.regexp "%[a-z0-9]+" in + let regexp = Str.regexp "%%\\|%[a-z0-9]+" in try ignore (Str.search_forward regexp cmdl 0); (* Try to find one match *) Str.global_substitute regexp substitute cmdl