From 46ba9b95a3ad827236b015fee5cac2d5bb53024d Mon Sep 17 00:00:00 2001
From: Michael Kraus <michael.kraus@ipp.mpg.de>
Date: Mon, 23 Nov 2020 13:55:02 +0100
Subject: [PATCH] Minor update of Documenter workflow.

---
 .github/workflows/Documentation.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/Documentation.yml b/.github/workflows/Documentation.yml
index 89356d9..fb98d01 100644
--- a/.github/workflows/Documentation.yml
+++ b/.github/workflows/Documentation.yml
@@ -15,11 +15,11 @@ jobs:
       - uses: julia-actions/setup-julia@latest
         with:
           version: 1.5
-      - name: set environment variables
+      - name: Set environment variables
         run: echo "PYTHON=''" >> $GITHUB_ENV
       - name: Install dependencies
-        run: julia --project=docs/ -e 'using Pkg; Pkg.develop(PackageSpec(path=pwd())); Pkg.instantiate()'
+        run: julia --project=docs/ -e 'using Pkg; Pkg.develop(PackageSpec(path=pwd())); Pkg.instantiate(); Pkg.build(); Pkg.precompile();'
       - name: Build and deploy Documentation
+        run: julia --project=docs/ docs/make.jl
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: julia --project=docs/ docs/make.jl