common/bin/idea.sh
changeset 37976 9cc5debe0f47
parent 37861 53d85619d7fe
--- a/common/bin/idea.sh	Thu May 19 17:24:50 2016 +0200
+++ b/common/bin/idea.sh	Thu May 19 16:48:43 2016 +0100
@@ -155,6 +155,14 @@
   printf "%s\n" "$mn" >> $IDEA_ANT
 }
 
+JTREG_HOME="        <property name=\"jtreg.home\" value=\"####\" />"
+
+addJtregHome() {
+  DIR=`dirname $SPEC`
+  mn="`echo "$JTREG_HOME" | sed -e s@"\(.*\)####\(.*\)"@"\1$JT_HOME\2"@`"
+  printf "%s\n" "$mn" >> $IDEA_ANT
+}
+
 ### Generate ant.xml
 
 rm -f $IDEA_ANT
@@ -162,6 +170,8 @@
 do
   if echo "$line" | egrep "^ .* <property name=\"module.name\"" > /dev/null ; then
     addModuleName
+  elif echo "$line" | egrep "^ .* <property name=\"jtreg.home\"" > /dev/null ; then
+    addJtregHome
   elif echo "$line" | egrep "^ .* <property name=\"build.target.dir\"" > /dev/null ; then
     addBuildDir
   else