summaryrefslogtreecommitdiffstats
path: root/site/posts/ClightIntroduction.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-07-14 11:26:58 +0200
committerThomas Letan <lthms@soap.coffee>2020-07-14 11:26:58 +0200
commitc62a61dba7285a034fc0405edbd47dcc48bf03f5 (patch)
tree994a21ae6741acb026e73a8d0e85933f04562732 /site/posts/ClightIntroduction.v
parentIdentify the creation and last update date from the revisions table (diff)
Prepare the introduction of a RSS feed
Diffstat (limited to 'site/posts/ClightIntroduction.v')
-rw-r--r--site/posts/ClightIntroduction.v7
1 files changed, 3 insertions, 4 deletions
diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v
index 0d53f33..13bf773 100644
--- a/site/posts/ClightIntroduction.v
+++ b/site/posts/ClightIntroduction.v
@@ -8,10 +8,9 @@ Import ListNotations.
you write is preserved by CompCert compilation passes up to the generated
machine code.
- I have been interested in CompCert for quite some times now. Today (#<span
- id="time">#March 18, 2020#</span>#), I have challenged myself to study
- Clight and its semantics. This write-up is the result of this challenge,
- written as I was progressing.
+ I had been interested in CompCert for quite some times, and ultimately
+ challenged myself to study Clight and its semantics. This write-up is the
+ result of this challenge, written as I was progressing.
#<div id="generate-toc"></div>#