make the preloader's required profiler argument (time|notime) an optional switch: -pp

fixes for broken Windows batch files
This commit is contained in:
chocolateboy
2013-05-08 05:10:19 +01:00
committed by Nikolay Krasko
parent 5ca4df3d1d
commit 1bf06f7c02
4 changed files with 58 additions and 12 deletions
+7 -2
View File
@@ -2,7 +2,7 @@
#
##############################################################################
# Copyright 2002-2011, LAMP/EPFL
# Copyright 2011, JetBrains
# Copyright 2011-2013, JetBrains
#
# This is free software; see the distribution for copying conditions.
# There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A
@@ -45,6 +45,7 @@ fi
# -D options will be available as system properties.
declare -a java_args
declare -a kotlin_args
profile_preloader="notime"
while [ $# -gt 0 ]; do
case "$1" in
@@ -62,6 +63,10 @@ while [ $# -gt 0 ]; do
kotlin_args=("${kotlin_args[@]}" "$1")
shift
;;
-pp)
profile_preloader="time"
shift
;;
*)
kotlin_args=("${kotlin_args[@]}" "$1")
shift
@@ -82,4 +87,4 @@ CPSELECT="-cp "
$JAVA_OPTS \
"${java_args[@]}" \
${CPSELECT}"${KOTLIN_HOME}/lib/kotlin-preloader.jar" \
org.jetbrains.jet.preloading.Preloader "${KOTLIN_HOME}/lib/kotlin-compiler.jar" org.jetbrains.jet.cli.js.K2JSCompiler 4096 "$@"
org.jetbrains.jet.preloading.Preloader "${KOTLIN_HOME}/lib/kotlin-compiler.jar" org.jetbrains.jet.cli.js.K2JSCompiler 4096 $profile_preloader "$@"