dev: still copy Makefile

centre-for-humanities-computing · Oct 12, 2023 · 243dc9e · 243dc9e
1 parent 5fd7431
commit 243dc9e
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Dockerfile.dev b/Dockerfile.dev
@@ -10,7 +10,8 @@ COPY requirements-dev.txt ./
 RUN pip install -r requirements-dev.txt
 
 ## Run static-type-checks to initialise the cache
-RUN pyright .
+COPY Makefile ./
+RUN make type-check
 
 ## Initialise pre-commit
 ### Remove the .git repo afterwards, since the dev container bind-mounts the development repo