Lesenechal Remi
|
787d4689a0
|
dune clean in the coverage target makes it more stable
|
2019-12-31 14:23:51 +01:00 |
|
Lesenechal Remi
|
46ac00e94d
|
makefile target
|
2019-12-31 14:23:51 +01:00 |
|
Tom Jack
|
8e8824c74a
|
Always run setup_repos.sh, never setup_dev_switch.sh, upon make build-deps
|
2019-09-27 08:43:57 -05:00 |
|
Tom Jack
|
e700c13897
|
Makefile cleanup
|
2019-09-09 14:35:18 -07:00 |
|
Georges Dupéron
|
644d90be6d
|
Fix CI and Makefile (WIP)
|
2019-09-06 17:27:09 +02: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 |
|