From 3ff90bcd36ecb58a6c385ef9696f8a910a3aff7d Mon Sep 17 00:00:00 2001
From: Idir Lankri <ilankri@besport.com>
Date: Mon, 28 Mar 2022 15:43:54 +0200
Subject: [PATCH] [cleanup] Remove outdated file `.jenkins.sh`

---
 .jenkins.sh | 15 ---------------
 1 file changed, 15 deletions(-)
 delete mode 100644 .jenkins.sh

diff --git a/.jenkins.sh b/.jenkins.sh
deleted file mode 100644
index a4f44dec1..000000000
--- a/.jenkins.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-opam pin add --no-action ocsigenserver .
-opam install --deps-only ocsigenserver
-opam install --verbose ocsigenserver
-
-do_build_doc () {
-  make -C doc clean
-  make -C doc doc
-  make -C doc wikidoc
-  cp -rf doc/api-wiki/*.wiki ${API_DIR}
-  cp -rf doc/manual-wiki/*.wiki ${MANUAL_SRC_DIR}
-}
-
-do_remove () {
-  opam remove --verbose ocsigenserver
-}