Always enable git metadata, fetch whole git history in pages CI (UniM…

…ath#785)

.github/workflows/pages.yaml

@@ -40,6 +40,8 @@ jobs:
         uses: actions/checkout@v3
         with:
           path: master
+          # We need the entire history for contributor information
+          fetch-depth: 0
 
       - name: Setup Agda
         uses: wenkokke/[email protected]

book.toml

@@ -29,7 +29,7 @@ command = "./scripts/preprocessor_git_metadata.py"
 # Disable by default - it takes a non-trivial amount of time
 # Can be overriden by running
 # `export MDBOOK_PREPROCESSOR__GIT_METADATA__ENABLE=true` in your shell
-enable = false
+enable = true
 # Only show "Content created by" on Agda source files
 attribute_file_extensions = [ ".lagda.md" ]
 # Don't add anything to the "non-content" pages,