From a3d7f5bc17aa3935a427812a49de60ecc0a345ca Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 24 Sep 2012 09:26:45 +0100 Subject: generator: The default input files are 'generator/ *.ml' [sic]. Since generator source files were renamed, the comment at the top of each generated file was wrong. Unfortunately we cannot allow /* to appear within a comment, so the space is necessary. --- generator/docstrings.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'generator/docstrings.ml') diff --git a/generator/docstrings.ml b/generator/docstrings.ml index 3faaa57c..7a32cb9c 100644 --- a/generator/docstrings.ml +++ b/generator/docstrings.ml @@ -62,7 +62,7 @@ type comment_style = type license = GPLv2plus | LGPLv2plus let generate_header ?(extra_inputs = []) comment license = - let inputs = "generator/generator_*.ml" :: extra_inputs in + let inputs = "generator/ *.ml" :: extra_inputs in let c = match comment with | CStyle -> pr "/* "; " *" | CPlusPlusStyle -> pr "// "; "//" -- cgit