projects / grub.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fd0df6d) | patch
Fix "make -C docs dvi"
authorColin Watson <cjwatson@ubuntu.com>
Fri, 29 Nov 2013 13:48:23 +0000 (13:48 +0000)
committerColin Watson <cjwatson@ubuntu.com>
Fri, 29 Nov 2013 13:48:23 +0000 (13:48 +0000)
commit8ddf84bfb8df5ae06498c98e336f359628a6c5ef
tree041d905a1b013ec8d6038be079c1783598808272tree | snapshot
parentfd0df6d098b1e6a4f60275c48a3ec88d15ba1fbbcommit | diff
Fix "make -C docs dvi"

* docs/grub-dev.texi (Font Metrics): Exclude @image command from DVI
builds, since we don't have an EPS version of font_char_metrics.png.
Add leading dot to image extension per the Texinfo documentation.
ChangeLog diff | blob | history
docs/grub-dev.texi diff | blob | history
GRUB2 development