Merge branch 'master' into firedrake

firedrakeproject · Feb 18, 2020 · 0d9a514 · 0d9a514
2 parents 4972004 + bac983c
commit 0d9a514
Show file tree

Hide file tree

Showing 1,349 changed files with 49,031 additions and 14,755 deletions.
diff --git a/.gitignore b/.gitignore
@@ -10,6 +10,7 @@
 *.pvt[ksu]
 *.h5m
 .*_license
+*.mypy_cache
 unix/*
 unix-opt/*
 unix-gcov/*