diff --git a/Makefile b/Makefile index b907e3228..173db8186 100644 --- a/Makefile +++ b/Makefile @@ -82,7 +82,7 @@ MANAGE += py.build py.clean MANAGE += pyenv pyenv.install pyenv.uninstall MANAGE += pypi.upload pypi.upload.test MANAGE += test.yamllint test.pylint test.pep8 test.unit test.coverage test.robot test.clean -MANAGE += themes.all themes.oscar themes.simple themes.bootstrap +MANAGE += themes.all themes.oscar themes.simple themes.bootstrap pygments.less PHONY += $(MANAGE) diff --git a/manage b/manage index 64d46616b..c741dfb81 100755 --- a/manage +++ b/manage @@ -86,6 +86,8 @@ themes.* : all : build all themes oscar : build oscar theme simple : build simple theme +pygments.* : + less : build LESS files for pygments EOF } @@ -326,7 +328,6 @@ node.clean() { } pygments.less() { - [ "$_pyenv_OK" == "OK" ] && return 0 build_msg PYGMENTS "searx_extra/update/update_pygments.py" if ! pyenv.cmd python searx_extra/update/update_pygments.py; then build_msg PYGMENTS "building LESS files for pygments failed"