From 9e100f919623aeb6a4cf2cfb10ff6529f3e7e3de Mon Sep 17 00:00:00 2001
From: Mark Andrews <marka@isc.org>
Date: Fri, 8 May 2020 14:34:34 +1000
Subject: [PATCH] remove xmllint of .html files

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

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e1627c0dd4..5ddb268400 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -394,7 +394,6 @@ misc:
     - perl -w util/update_copyrights < util/copyrights
     - if test "$(git status --porcelain | grep -Ev '\?\?' | wc -l)" -gt "0"; then git status --short; exit 1; fi
     - xmllint --noout --nonet `git ls-files '*.xml' '*.docbook'`
-    - xmllint --noout --nonet --html `git ls-files '*.html'`
     - sh util/check-win32util-configure
     - sh util/check-categories.sh
   needs: []