From e3b6075966ab583368e7cfe32122c46e2bea3e6e Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 26 Sep 2023 18:16:03 +0200
Subject: [PATCH] Ensure that working directory doesn't stay in the plastex
directory
---
.gitlab-ci.yml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a2f6a9a..643c139 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -8,7 +8,7 @@ build:
- apt-get install -y ant dvipng maven python-imaging rubber texlive-fonts-recommended texlive-latex-extra texlive-math-extra wget
- wget -O plastex.tar.gz https://github.com/tiarno/plastex/archive/1.0.0.tar.gz
- tar -xzvf plastex.tar.gz
- - cd plastex-1.0.0 && python setup.py install
+ - (cd plastex-1.0.0 && python setup.py install)
script:
- cd org.rodinp.handbook.feature
- ant -file customBuild.xml
--
GitLab