From dac0aadbb00447f4bbfe40586d32ccffe6703222 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 6 Dec 2021 23:32:46 +0100
Subject: Revert "fix"

This reverts commit 9370eee7cdbe07888aa749f4f9153c1cab3bff56.
---
 .gitlab-ci.yml | 1 -
 1 file changed, 1 deletion(-)

(limited to '.gitlab-ci.yml')

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b200eba6..728bd3c3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -330,7 +330,6 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil
   rules:
     - if: '$CI_COMMIT_BRANCH == "master"'
       when: always
-    - when: manual
 
 build_aarch64_coq13:
   stage: build
-- 
cgit