IntenseWebs/pgadmin4
3
0
Fork 0
mirror of https://github.com/pgadmin-org/pgadmin4.git synced 2025-02-25 18:55:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

Use config_distro.py for all settings, and don't create/overwrite config_local.py. Partly fixes #1849

Browse Source
This commit is contained in:
Sandeep Thakkar
2016-10-19 14:10:28 +01:00
committed by Dave Page
parent 19df1e3f4b
commit a1c0042a1e
2 changed files with 3 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
Make.bat
View File

@@ -247,9 +247,6 @@ GOTO:EOF
ECHO HELP_PATH = '../../../docs/en_US/html/' >> "%PGBUILDPATH%\web\config_distro.py"
ECHO MINIFY_HTML = False >> "%PGBUILDPATH%\web\config_distro.py"
ECHO Creating config_local.py
ECHO # Add any configuration changes to this file. > "%PGBUILDPATH%\web\config_local.py"
ECHO Building docs...
MKDIR "%PGBUILDPATH%\docs\en_US\html"
IF %ERRORLEVEL% NEQ 0 EXIT /B %ERRORLEVEL%