Bug 1251324 - Add a --disable-js-shell option to js/src/configure. r=chmanchester

This commit is contained in:
Mike Hommey 2016-03-09 15:27:42 +09:00
parent b16675c10b
commit 06634bfcb4
3 changed files with 7 additions and 3 deletions

View File

@ -3,3 +3,10 @@
# This Source Code Form is subject to the terms of the Mozilla Public
# License, v. 2.0. If a copy of the MPL was not distributed with this
# file, You can obtain one at http://mozilla.org/MPL/2.0/.
option('--disable-js-shell', help='Do not build the JS shell')
@depends('--disable-js-shell')
def js_shell(value):
if not value:
set_config('JS_DISABLE_SHELL', '1')

View File

@ -53,7 +53,6 @@ with Files('../public/TrackedOptimizationInfo.h'):
if CONFIG['JS_BUNDLED_EDITLINE']:
DIRS += ['editline']
# editline needs to get built before the shell
if not CONFIG['JS_DISABLE_SHELL']:
DIRS += ['shell']

View File

@ -3273,7 +3273,6 @@ MOZ_ARG_ENABLE_BOOL(readline,
JS_BUNDLED_EDITLINE=
EDITLINE_LIBS=
JS_DISABLE_SHELL=
case "$target" in
*-mingw*)
@ -3297,7 +3296,6 @@ if test -z "$SKIP_LIBRARY_CHECKS" -a -z "$NO_EDITLINE"; then
AC_DEFINE(EDITLINE)
fi
AC_SUBST(JS_BUNDLED_EDITLINE)
AC_SUBST(JS_DISABLE_SHELL)
AC_SUBST_LIST(EDITLINE_LIBS)
dnl ========================================================