aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--README.md (renamed from README)21
1 files changed, 8 insertions, 13 deletions
diff --git a/README b/README.md
index e9492973..32b419a7 100644
--- a/README
+++ b/README.md
@@ -1,7 +1,7 @@
- The CompCert C verified compiler
-
-OVERVIEW:
+# CompCert
+The verified C compiler.
+## Overview
The CompCert C verified compiler is a compiler for a large subset of the
C programming language that generates code for the PowerPC, ARM and x86
processors.
@@ -17,18 +17,13 @@ purposes.
For more information on CompCert (supported platforms, supported C
features, installation instructions, using the compiler, etc), please
-refer to the user's manual: http://compcert.inria.fr/man/
-
-
-COPYRIGHT:
+refer to the [user's manual](http://compcert.inria.fr/man/).
+## Copyright
The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007,
2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut National de Recherche en
Informatique et en Automatique (INRIA). It is distributed under the
-conditions stated in file LICENSE.
-
-
-CONTACT:
-
-The authors can be contacted by e-mail at compcert@yquem.inria.fr
+conditions stated in file `LICENSE`.
+## Contact
+The authors can be contacted by e-mail at compcert@yquem.inria.fr.