Add update git server if needed (#20)

This commit is contained in:
Roman Demidov
2019-12-12 18:21:24 +03:00
committed by Alexey Golubev
parent cf7311f81f
commit 14c358e04a
3 changed files with 5 additions and 8 deletions

View File

@ -57,7 +57,7 @@ if ("1" == config.option("update")):
if config.check_option("module", "desktop"):
base.git_update("desktop-apps")
if config.check_option("module", "develop"):
if(config.check_option("module", "develop") or config.check_option("module", "server")):
base.git_update("server")
base.git_update("document-server-integration")
base.git_update("core-fonts")