[Pkg-jed-devel] error building jed_0.99.16.pre.0.99.17.84-1

[G. Milde]

On 13.04.05, Rafael Laboissiere wrote:
> * Jörg Sommer <joerg@alea.gnuu.de> [2005-04-13 22:05]:
> 
> > I've get an error when I try to build the new jed version. I don't know
> > if it is also a problem of older version.
> > 
> > The problem happens when the jed-extra package is installed. While the
> > build jed is run to byecompile some file. For this it loads /etc/jed.conf
> > and /etc/jed-init.d/50jed-extra.sl which tries to load jed-extra, but
> > that isn't in the path while building with the just now build version of
> > jed.
> 
> I have already noticed this problem, but forgot to find a solution for
> it. In my sid chroot I simply removed (and purged) the jed-extra package.
> We could build-conflict on jed-extra, but this is not a satisfying
> solution.

Would'nt it be sufficient to move /etc/jed-init.d/50jed-extra.sl out of the
way (e.g. temporarily rename to 50jed-extra.sl.old or delete if it is no
longer needed (in this version))?

 
> > Or should we modify site.sl to not load /etc/jed.conf at this point? 

Rather modify jed.conf - 
  site.sl is in the jed standard distribution and should be left as-is, 
  jed.conf is a Debian extension, so the debian package is free to change
  this.
 

Another idea would be to use a command line argument to set a variable
and check for it in jed.conf (with a custom_variable as default).

Example: as home-lib.sl does this kind of checking, I should be able to
use this scheme for the non-loading of the ini.sl file in my local jed
library:
 
   jed -f 'variable Jed_Home_Library = ""'

However, my tests revealed that the evaluation of this argument appeares
after the reading of home-lib.sl so that the jed-library-path is alredy set.

The next idea is using environment variables, like

   JED_HOME="foo"; jed

this works as expected: the Jed_Home_Library is not added to the
jed-library-path and Jed_Home_Library/ini.sl is not evaluated.

Maybe this could be adapted to the above problem.

Günter


-- 
G.Milde web.de