update of jed-extra

[G. Milde]

On 11.07.05, Jörg Sommer wrote:
> G. Milde schrieb am Mon 11. Jul, 09:44 (+0200):
> > On  6.07.05, Jörg Sommer wrote:
> > > 
> > > ... I would introduce a directory for documentations like it is
> > > done with JED_ROOT/doc to make it possible move the documentation
> > > to /usr/share/doc/.
 
> Yes, but where to put the documentation of non JED libs? E.g. where to
> put the (not existing) documentation of site-lib?

The link /usr/share/doc/jed -> JED_ROOT/doc is only needed for the 
Help>Browse_Docs menu entry (looking for files in JED_ROOT/doc/txt). No
similar link is needed for extensions as no provision exists to extend
the search path of Help>Browse_Docs.

I'd do it similar to jed-common: online-help files (*.hlp) go into the
library dir itself, additional documentation goes to /usr/share/doc.

A special case are function and variable descriptions generated with
tm_make_doc().

  * jed-common places them in /usr/share/jed/doc/txt and sets
    Jed_Doc_Files accordingly.

  * make_ini.sl places them in <libdir>/libfuns.txt and home-lib 
    expands Jed_Doc_Files accordingly.
    
If we generate this doc at build time, it should go to
/u/s/d/<package>/txt and jed-init.d/XX<package>.sl should expand
Jed_Doc_Files.

If we generate the libfuns (together with slc and dfa files) with
make-ini, I would prefer placing in <libdir>.

Günter


-- 
G.Milde web.de