'make draft' and HTML.index

Поиск
Список
Период
Сортировка
От Alvaro Herrera
Тема 'make draft' and HTML.index
Дата
Msg-id 20080109054155.GG20913@alvh.no-ip.org
обсуждение исходный текст
Ответы Re: 'make draft' and HTML.index
Список pgsql-docs
I just noticed that I can very quickly generate an up-to-date HTML.index
by commenting out normal HTML generation, i.e. patching html/docbook.dsl
thusly:

*** docbook.dsl.orig    2008-01-09 02:35:53.000000000 -0300
--- docbook.dsl 2008-01-09 02:35:12.000000000 -0300
***************
*** 102,110 ****
  ;(define (docelem node)
  ;  (node-propety 'document-element
  ;    (node-property 'grove-root node)))
!    (process-children)
!    (with-mode manifest
!      (process-children))
     (if html-index
         (with-mode htmlindex
         (process-children))
--- 102,110 ----
  ;(define (docelem node)
  ;  (node-propety 'document-element
  ;    (node-property 'grove-root node)))
! ;   (process-children)
! ;   (with-mode manifest
! ;     (process-children))
     (if html-index
         (with-mode htmlindex
         (process-children))

(Of course, this suppresses normal HTML output).

Currently, we generate HTML.index by running openjade in normal mode,
and then rerunning if we detect that the HTML.index file changed.  This
is a waste -- with patched docbook.dsl, it takes 8 seconds to generate
the index file on my system, whereas the regular openjade run takes
1:30.  So on a clean start it takes 3 minutes to generate the docs.

This could be reduced to 1:38 if we were to generate the HTML.index file
with a hack similar to the above, and then run openjade only once.
However, I have no idea if we can ship a .dsl file and convince openjade
to run with that instead of the normal docbook.dsl.

--
Alvaro Herrera                                http://www.CommandPrompt.com/
The PostgreSQL Company - Command Prompt, Inc.

В списке pgsql-docs по дате отправления:

Предыдущее
От: Bruce Momjian
Дата:
Сообщение: Re: Partitioning documentation example
Следующее
От: Tom Lane
Дата:
Сообщение: Re: 'make draft' and HTML.index