From: Michal Sojka <sojkam1@fel.cvut.cz>
Date: Tue, 12 Nov 2013 08:30:26 +0000 (+0100)
Subject: Use synctex to ease documentation editting
X-Git-Url: https://rtime.felk.cvut.cz/gitweb/omk.git/commitdiff_plain/60a244e8e5c817b7d501eaf2e9008e44bc882329?hp=66c9d3697310ae7c760b3524acdceee4e00936c8

Use synctex to ease documentation editting
---

diff --git a/doc/Makefile b/doc/Makefile
index 87dd9a5..81db85f 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -28,6 +28,10 @@ tests/%:
 %.pdf: %.png
 	convert $< -density 150 $@
 
+# We want to use synctex. texi2dvi does not support this directly, so
+# we use the PDFTEX variable for this.
+export PDFTEX = pdfetex -synctex=1
+
 %.pdf: %.texinfo $(PNG_FIGS) $(MANUAL_INCLUDES)
 	texi2dvi --pdf $<
 	texi2dvi --pdf $<