Re: How do I set different JAVA_HOME for different users?

["Thomas Schmitt" <scdbackup@gmx.net>]

Hi,

> The trouble is, often you need to know where to look,

The collective brain here always has interesting proposals. :))


> A shell script exactly like that was what what I started out with!
> It worked ONLY for that terminal.

You'd need to put start of the whole android development into that
script. So that all processes started for that purpose inherit the
variable.


> I never thought to try 'man bash'.

It can be frustrating to search for answers in there.
Often you find the explanation why it works only after inventing a
way how it works.

In this case, bash is only involved as a common ancestor of all
your user's activity. When new processes get started, they normally
are subject to these statements from man 2 fork, when the parent process
duplicates itself:

  The
  new process, referred to as the child, is an  exact  duplicate  of  the
  calling  process,  referred  to as the parent, except for the following
  points: [... none of them applies to environment variables ...]

and man 3 execl, when the child process replaces the parent program by
the program which shall get started:

  For those forms not containing an envp pointer ( execl(), execv(), exe‐
  clp(),  and  execvp()), the environment for the new process image shall
  be taken from the external variable environ in the calling process.


Other ancestor programs (like systemd or the desktop) may of course
decide not to forward all their environment but construct a new set
of variables for those processes which they launch.


Have a nice day :)

Thomas