comparison make-dist @ 31660:84c9abde389f

(Info-fontify-node): Make a few cleanups. Add extra `help-echo' and `local-map' props to node xrefs. Use header-specific faces for node-names & xrefs. (Info-use-header-line, Info-header-line): New variables. (info-header, info-header-xref, info-header-node): New faces. (Info-setup-header-line): New function. (Info-select-node): Call Info-setup-header-line when enabled. (Info-extract-pointer): Work even if the header line is hidden.
author Miles Bader <miles@gnu.org>
date Sun, 17 Sep 2000 16:20:35 +0000
parents 28cc44c6c08c
children f50932a70105
comparison
equal deleted inserted replaced
31659:fa8b259c5ce4 31660:84c9abde389f