Re: Where is push_defaults?

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

On  3.04.06, Dave Laird wrote:
> Good morning, Gunther...
> 
> On Monday 03 April 2006 08:23 am, G. Milde wrote:
>  
> > Try to locate sl_utils.sl and put it in your jed library path. 
 
> Done. In fact, I've tried three different versions, just in case there was
> a problem, but I just found it. 

BTW, the current version is % 2005-10-05 1.5.3, but with anything newer than
1.4 you should be ok.

 
> message(get_jed_library_path) returns /usr/local/jed/lib which in where
> Jed libs are located. Harumph. 

I recommend to keep local extensions (as e.g. modes from jedmodes or
homebrewn or modified ones) in a separate directory. This way they will
be easy distinguishable from the canonic modes and never be overwritten
by a new version of Jed.


In my jed.rc I define several extensions using libdir.sl from
jedmodes.sf.net:

  %-----------------------------------------------------------------------
  % Extension Libraries and Jed_Home_Directory ("~/.jed")
  
  % insert("loading home-lib");
  require("/home/milde/.jed/lib/libdir.sl"); 
  add_libdir(path_concat(Jed_Home_Directory, "lib"));
  Jed_Highlight_Cache_Dir = path_concat(Jed_Home_Directory, "lib");
  % make slsh skripts available in jed
  set_jed_library_path(strcat(get_jed_library_path(),
  			    ",", "/usr/share/slsh/local-packages"));
  append_libdir("/usr/share/slsh");


where the current Debian jed package defines a users Jed_Home_Directory in
/etc/jed.d/05jed-common.sl as follows:

% Jed_Home_Directory (defined in site.sl, defaulting to $HOME)
% 
% If a subdir .jed/ exists, point Jed_Home_Directory there, 
% so .jedrc and .jedrecent are not spoiling the $HOME dir (FHS 2.3)
$1 = path_concat(Jed_Home_Directory, ".jed");
if ( 2 == file_status($1) ) {
   Jed_Home_Directory = $1;
   % set the default jedrc file path to ~/.jed/jed.rc
   Default_Jedrc_Startup_File = path_concat(Jed_Home_Directory, "jed.rc");
}


Günter

-- 
Milde ife.et.tu-dresden.de

--------------------------
To unsubscribe send email to <jed-users-request@xxxxxxxxxxx> with
the word "unsubscribe" in the message body.
Need help? Email <jed-users-owner@xxxxxxxxxxx>.