From cf3f9615d79e0cbe4eb146c08e2c0802e1e3f033 Mon Sep 17 00:00:00 2001
From: Michael Schmidt <github@mschmidt.me>
Date: Mon, 25 Apr 2016 17:42:27 +0200
Subject: bug 18004, fix file extensions for dparse option

---
 exportclight/Clightgen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'exportclight')

diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index d917032e..cbc2d8c4 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -211,7 +211,7 @@ Language support options (use -fno-<opt> to turn off -f<opt>) :
   -fall          Activate all language support options above
   -fnone         Turn off all language support options above
 Tracing options:
-  -dparse        Save C file after parsing and elaboration in <file>.parse.c
+  -dparse        Save C file after parsing and elaboration in <file>.parsed.c
   -dc            Save generated Compcert C in <file>.compcert.c
   -dclight       Save generated Clight in <file>.light.c
 General options:
-- 
cgit