From 4fef9336a2ccd25fc3ab96284b6d6a7065dee4c3 Mon Sep 17 00:00:00 2001
From: hferee <hferee@users.noreply.github.com>
Date: Thu, 12 Sep 2024 21:56:55 +0200
Subject: [PATCH] Update build_docs.yml

Add build times artifact
---
 .github/workflows/build_docs.yml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/build_docs.yml b/.github/workflows/build_docs.yml
index 1a95d52..00ae9b1 100644
--- a/.github/workflows/build_docs.yml
+++ b/.github/workflows/build_docs.yml
@@ -33,7 +33,7 @@ jobs:
             startGroup "Build project"
               opam update -y
               ./install.sh -y
-              make -j 4
+              make -j 4 pretty-timed
               make -j 4 doc
               dune exec benchmark > benchmark.md
             endGroup
@@ -53,6 +53,11 @@ jobs:
         with:
           name: benchmark
           path: benchmark.md
+      - name: Upload build time log
+        uses: actions/upload-artifact@master
+        with:
+          name: build-time
+          path: time-of-build-pretty.log
 
       - name: Revert permissions
         # to avoid a warning at cleanup time