Removing unneeded files.

#! /usr/bin/env bash

# ----------------------------------------------------

# This script builds documentation for gitlab-pages.

#

# ----------------------------------------------------

cd ${NCP_TOP_LEVEL}/documentation

make -f Makefile-gitlab-pages clean && make -f Makefile-gitlab-pages html

if [[ $? != 0 ]]; then

    echo "Failed to create documentation."

    exit 1

else

    echo "Created documentation."

fi

# Minimal makefile for Sphinx documentation

#

# You can set these variables from the command line, and also

# from the environment for the first two.

SPHINXOPTS    ?=

SPHINXBUILD   ?= sphinx-build

SOURCEDIR     = source

BUILDDIR      = $(NCP_TOP_LEVEL)/public

# Put it first so that "make" without argument is like "make help".

help:

	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)

.PHONY: help Makefile

# Catch-all target: route all unknown targets to Sphinx using the new

# "make mode" option.  $(O) is meant as a shortcut for $(SPHINXOPTS).

%: Makefile

	@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)