From be97164d42971ecda7f3b5c9e3f1bec0a73094e4 Mon Sep 17 00:00:00 2001
From: Raymond Toy <toy.raymond@gmail.com>
Date: Sun, 15 Jul 2018 17:36:46 -0700
Subject: [PATCH] Build the HTML user manual

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 284c42249..7e15b61cb 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -16,6 +16,7 @@ linux-runner:
     - bin/build.sh -C "" -o snapshot/bin/lisp
     - bin/make-dist.sh -I dist linux-4
     - bin/run-tests.sh -l dist/bin/lisp 2>&1 | tee test.log
+    - (cd src/docs/cmu-user; make cmu-user.html)
 
 osx-runner:
   tags:
-- 
GitLab