diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-05-28 07:27:46 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-05-28 07:27:46 +0200 |
commit | e7fad4516e0e7705480312caa427e838f3321948 (patch) | |
tree | 8a56b3e91a9ad3262137d15cca44913b56dbd803 | |
parent | a1358ff333c840ac0ac447d6f55d64cc7d077cc4 (diff) | |
download | compcert-kvx-e7fad4516e0e7705480312caa427e838f3321948.tar.gz compcert-kvx-e7fad4516e0e7705480312caa427e838f3321948.zip |
automatic date in the html index
-rw-r--r-- | .gitlab-ci.yml | 7 | ||||
-rw-r--r-- | doc/index-kvx.html | 2 | ||||
-rwxr-xr-x | tools/fix_html_date.sh | 8 |
3 files changed, 13 insertions, 4 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 971034bc..0499abc2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -258,8 +258,8 @@ build_kvx: when: always - when: manual -pages: - stage: build # TODO: change to "deploy" when "build" succeeds +pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "build_kvx" above ?) + stage: build image: "coqorg/coq" before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update @@ -280,7 +280,8 @@ pages: - source /opt/kalray/accesscore/kalray.sh && make documentation - mkdir public - cp -r doc/* public/ - - mv public/index-kvx.html public/index.html + - tools/fix_html_date.sh doc/index-kvx.html " (" ")" > public/index.html + - rm public/index-kvx.html artifacts: paths: - public diff --git a/doc/index-kvx.html b/doc/index-kvx.html index 4660c1d1..95fdb6de 100644 --- a/doc/index-kvx.html +++ b/doc/index-kvx.html @@ -25,7 +25,7 @@ a:active {color : Red; text-decoration : underline; } <font color=gray><H1 align="center">The CompCert verified compiler</H1> <H2 align="center">Commented Coq development</H2> <H3 align="center">Version 3.7, 2020-03-31</H3></font> -<H3 align="center">PATCHED for the Kalray MPPA-KVX VLIW CORE (2020-05-27)</H3> +<H3 align="center">PATCHED for the Kalray MPPA-KVX VLIW CORE<!--@DATE@--></H3> <H2>Introduction</H2> diff --git a/tools/fix_html_date.sh b/tools/fix_html_date.sh new file mode 100755 index 00000000..c7fbdabe --- /dev/null +++ b/tools/fix_html_date.sh @@ -0,0 +1,8 @@ +#!/bin/bash +# +# Replace an HTML comment "<!--@DATE@-->" by the current date +# in the file given by $1 (with $2 as prefix and $3 as suffix) +# +# Result on standard output + +sed -e "s/<!--@DATE@-->/$2$(date +'%F')$3/g" $1 |