aboutsummaryrefslogtreecommitdiffstats
path: root/doc/coq2html.mll
diff options
context:
space:
mode:
authorMichael Schmidt <github@mschmidt.me>2015-10-14 15:07:48 +0200
committerMichael Schmidt <github@mschmidt.me>2015-10-14 15:07:48 +0200
commit60ab550a952c3d9719b2a91ec90c9b58769f6717 (patch)
tree523cf4eb5a35594b16a297b4bd7e29157f42b0fc /doc/coq2html.mll
parenta479c280441b91007c379b0b63b907926d54f930 (diff)
downloadcompcert-60ab550a952c3d9719b2a91ec90c9b58769f6717.tar.gz
compcert-60ab550a952c3d9719b2a91ec90c9b58769f6717.zip
bug 17392: remove trailing whitespace in source files
Diffstat (limited to 'doc/coq2html.mll')
-rw-r--r--doc/coq2html.mll10
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/coq2html.mll b/doc/coq2html.mll
index 2f1bfdbc..7dd93842 100644
--- a/doc/coq2html.mll
+++ b/doc/coq2html.mll
@@ -157,7 +157,7 @@ let rec set_enum_depth d =
fprintf !oc "<ul>\n";
fprintf !oc "<li>\n";
incr enum_depth;
- end
+ end
else if !enum_depth > d then begin
fprintf !oc "</li>\n";
fprintf !oc "</ul>\n";
@@ -290,7 +290,7 @@ rule coq_bol = parse
| eof
{ () }
| space* as s
- { space s;
+ { space s;
coq lexbuf }
and skip_newline = parse
@@ -337,7 +337,7 @@ and comment = parse
| "*)"
{ if !in_proof then end_comment() }
| "(*"
- { if !in_proof then start_comment();
+ { if !in_proof then start_comment();
comment lexbuf; comment lexbuf }
| eof
{ () }
@@ -345,7 +345,7 @@ and comment = parse
{ if !in_proof then newline();
comment lexbuf }
| space* as s
- { if !in_proof then space s;
+ { if !in_proof then space s;
comment lexbuf }
| eof
{ () }
@@ -422,7 +422,7 @@ let process_file f =
if Filename.check_suffix f ".v" then begin
let pref_f = Filename.chop_suffix f ".v" in
let base_f = Filename.basename pref_f in
- current_module :=
+ current_module :=
"compcert." ^ Str.global_replace (Str.regexp "/") "." pref_f;
let ic = open_in f in
if !output_name = "-" then