| commit | edfd7cd4c0becb33be812b578afd4d226ba53f1c | [log] [tgz] |
|---|---|---|
| author | Romain Manni-Bucau <rmannibucau@gmail.com> | Mon Nov 04 17:56:48 2019 +0100 |
| committer | Romain Manni-Bucau <rmannibucau@gmail.com> | Mon Nov 04 17:56:48 2019 +0100 |
| tree | 56c50c9f9e9d024bfa8e5cfa8a5f46e3f103cd9c | |
| parent | df2709a1117e4653c698e6f4e1715039cdae1fdf [diff] |
extracting website publication to a dedicated job in github actions (deactivated for now while we don't have secrets for it)