From 5df29e2caa1ec95a3ddbcaf49d686998b0696855 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 10 Jan 2018 10:32:43 +0100
Subject: Change README to markdown.

---
 exportclight/README    | 34 ----------------------------------
 exportclight/README.md | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 33 insertions(+), 34 deletions(-)
 delete mode 100644 exportclight/README
 create mode 100644 exportclight/README.md

(limited to 'exportclight')

diff --git a/exportclight/README b/exportclight/README
deleted file mode 100644
index 3fd8c0ae..00000000
--- a/exportclight/README
+++ /dev/null
@@ -1,34 +0,0 @@
-                        The clightgen tool
-                        ------------------
-
-OVERVIEW
-
-"clightgen" is an experimental tool that transforms C source files
-into Clight abstract syntax, pretty-printed in Coq format in .v files.
-These generated .v files can be loaded in a Coq session for
-interactive verification, typically.
-
-
-HOW TO BUILD
-
-Change to the top-level CompCert directory and issue
-
-          make clightgen
-
-
-USAGE
-
-        clightgen [options] <C source files>
-
-For each source file "src.c", its Clight abstract syntax is generated
-in "src.v".
-
-The options recognized are a subset of those of the CompCert compiler ccomp
-(see http://compcert.inria.fr/man/manual003.html for full documentation):
-
-   -I<dir>     search <dir> for include files
-   -D<symbol>  define preprocessor macro
-   -U<symbol>  undefine preprocessor macro
-   -Wp,<opts>  pass options to C preprocessor
-   -f<feature> activate emulation of the given C feature
-
diff --git a/exportclight/README.md b/exportclight/README.md
new file mode 100644
index 00000000..7252ff8a
--- /dev/null
+++ b/exportclight/README.md
@@ -0,0 +1,33 @@
+# The clightgen tool
+
+
+## Overview
+"clightgen" is an experimental tool that transforms C source files
+into Clight abstract syntax, pretty-printed in Coq format in .v files.
+These generated .v files can be loaded in a Coq session for
+interactive verification, typically.
+
+
+## How to build
+
+Change to the top-level CompCert directory and issue
+```
+   make clightgen
+```
+
+## Usage
+```
+   clightgen [options] <C source files>
+```
+For each source file "src.c", its Clight abstract syntax is generated
+in "src.v".
+
+The options recognized are a subset of those of the CompCert compiler ccomp
+(see [user's manual](http://compcert.inria.fr/man/manual003.html) for full documentation):
+```
+   -I<dir>     search <dir> for include files
+   -D<symbol>  define preprocessor macro
+   -U<symbol>  undefine preprocessor macro
+   -Wp,<opts>  pass options to C preprocessor
+   -f<feature> activate emulation of the given C feature
+```
-- 
cgit