Commit Graph

8 Commits

Author SHA1 Message Date
Rémi Lesenechal
8b83e375bd Revert "Merge branch 'feature/adt-generator-poly-3' into 'dev'"
This reverts merge request !403
2020-02-11 10:45:08 +00:00
Suzanne Dupéron
7bad718135 Add missing dependency on Python 3 2020-02-10 20:40:43 +01:00
Suzanne Dupéron
8f03d45ec3 Make more scripts print their commands, to help debug issues in GitLab 2020-02-10 20:40:43 +01:00
Tom Jack
c83813456a Relocate .opam 2019-12-16 22:50:25 +00:00
Pierre-Emmanuel Wulfman
f68e91466e Make install script works on archlinux 2019-10-24 13:04:16 +00:00
Georges Dupéron
47409db7db Started using the scripts/… in .gitignore, started a Makefile for one-liners to be used by the devs, e.g. make build-deps, make, make test 2019-06-10 10:19:49 +02:00
Georges Dupéron
17b413faee Security aspects for shell scripts (well, an attempt at that) 2019-06-10 10:19:49 +02:00
Matej Sima
5feba725cb Refactor docker image structure & CI 2019-05-27 17:43:39 +02:00