Re: [build] build.xml proposal

[Thierry Kormann <Th...@sophia.inria.fr>]

> In my local setup I have changed build.sh a little, to use
> JRE_HOME and JDK_HOME as separate environment variables.  
> If either is undefined I set it equal to JAVA_HOME,  so my build.sh
> would work with no modification in a more usual environment
> (e.g. when jdk and jre are matching revs).
> 
> My question is, do other people think I should commit this version
> of build.sh ?  As I said, it will behave just like the current build.sh
> unless you have set the JDK_HOME or JRE_HOME environment
> variables before running the script.

That's fine to me.

Thierry.

-- 
Thierry Kormann
email: Thierry.Kormann@sophia.inria.fr  http://www.inria.fr/koala/tkormann/
Koala/Dyade/Bull @ INRIA - Sophia Antipolis