Re: Disable jed.conf (was: Re: Intention of jed-script)

["G. Milde" <g.milde@xxxxxx>]

On 13.07.05, John E. Davis wrote:
> G. Milde <g.milde@xxxxxx> wrote:
> >This solves much problems, but not the following example:
> >
> >  My jed.conf extends the jed-library-path by a private directory
> >  "~/.jed/lib", where I store my private and modified modes.
> 
>   I do not believe that jed.conf should be doing things that can be
> done in the .jedrc file.  The main idea behind jed.conf is that it is
> to provide suitable defaults for all users on the system.  

I agree with you and admit I have chosen the wrong example.

The "real" problem is with the jed Debian package, that wants to store
Debian-provided scripts in a "jed-site-library" and extend the
jed-library-path accordingly. This should obviously be a default for all
users.

However, on some special occasions, the need arises to override this 
default. A command line option would be the easiest way to provide for
this. 

 
> As a compromise, what do you feel about the following patch to
> site.sl?  The idea is that if jed is installed in, e.g.,
> /usr/local/bin, then jed will try to load /usr/local/etc/jed.conf and
> not /etc/jed.conf.  

We discussed a similar change on pkg-jed-devel and concluded that in our
opinion "/usr/local/etc/jed.conf" and "/usr/etc/jed.conf" will not be
needed. A local installation can easily provide a (possibly empty)
"defaults.sl" instead, which will also prevent loading /etc/jed.conf.
(We assume that anyone installing a local jed version alongside a
distributed one (say Debian), will be sufficiently "advanced" to manage
this.

> Also, if the environment variable JED_CONF_DIR is
> set, then it will be used as the directory containing jed.conf.

This adds flexibility, and could be (ab)used for our means by e.g.

   JED_CONF_DIR="/foo"; jed
   
However, I would still prefer a command line option to go along with
"JED_HOME_DIR" and "-n" for jed.rc|.jedrc.

Thanks

Guenter


-- 
G.Milde web.de