Go to file
John David Pressman 90eecb6b4c Merge branch 'dev' into 'dev'
# Conflicts:
#   gitlab-pages/website/pages/en/index.js
2019-08-12 10:03:06 +00:00
docker Use sh, not bash 2019-06-10 10:23:18 +02:00
gitlab-pages Remove duplicate Tutorials button from the home page 2019-08-08 14:25:54 +00:00
packages typo in sed script 2019-05-27 13:10:29 +02:00
scripts Merge branch 'makefile' into 'dev' 2019-08-03 00:22:46 +00:00
src Fixed regression. Enabled type annotations for all expressions 2019-07-30 11:27:32 +02:00
vendors Merge branch 'dev' into feature/better-error-messages 2019-07-21 11:58:09 +02:00
.gitignore Removed "assert" as reserved. Enabled terminating ";" in lists. 2019-06-10 15:19:42 +02:00
.gitlab-ci.yml Small fixes to the doc and to the odoc build script 2019-06-20 21:11:37 +02:00
CONTRIBUTORS.md add MIT license 2019-05-25 15:52:12 +00:00
index.tar.gz update repository 2019-05-13 19:24:21 +00:00
LICENSE.md add MIT license 2019-05-25 15:52:12 +00:00
makefile Swap makefile-native test command with script, add script 2019-06-08 21:57:46 -07:00
Makefile 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
repo update repository 2019-05-13 19:24:21 +00:00
urls.txt update repository 2019-05-13 19:24:21 +00:00