From e30b28491e6eb38fe69c62e2244b2ccd9594ec51 Mon Sep 17 00:00:00 2001
From: SaillantNicolas <97436229+SaillantNicolas@users.noreply.github.com>
Date: Wed, 1 Mar 2023 15:10:17 +0100
Subject: [PATCH] add the url to the job log

---
 .github/workflows/build_doc.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/build_doc.yml b/.github/workflows/build_doc.yml
index a2ee453953d..acd68a1ff51 100644
--- a/.github/workflows/build_doc.yml
+++ b/.github/workflows/build_doc.yml
@@ -159,7 +159,8 @@ jobs:
         with:
           script: |
             const error = process.env.ERRORMSG
-            const msg = "There was an error while building the doc: \n"+error
+            const job_url = `${context.serverUrl}/cgal/cgal/actions/runs/${context.runId}`
+            const msg = "There was an error while building the doc: \n"+error + "\n" + job_url
             github.rest.issues.createComment({
               owner: "CGAL",
               repo: "cgal",