aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tools
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-14 18:29:02 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-06-08 23:27:08 +0200
commit871a9e65009990963c12359531ea2beeacb7386d (patch)
tree2726970832b00fbc7fa122ceda955d4995a508bd /doc/tools
parent01128a2ff774f0ef249ee54a67e88d49ae254a4d (diff)
gitlab: build sphinx doc in separate job
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/coqrst/repl/coqtop.py5
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index aeadce4c4..3ff00eaaf 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -41,10 +41,13 @@ class CoqTop:
the ansicolors module)
:param args: Additional arugments to coqtop.
"""
+ BOOT = True
+ if os.getenv('COQBOOT') == "no":
+ BOOT = False
self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop")
if not pexpect.utils.which(self.coqtop_bin):
raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin))
- self.args = (args or []) + ["-boot", "-color", "on"] * color
+ self.args = (args or []) + ["-boot"] * BOOT + ["-color", "on"] * color
self.coqtop = None
def __enter__(self):