Use synctex to ease documentation editting

diff --git a/doc/Makefile b/doc/Makefile
index 87dd9a5c2e10a340394d598b0e7a5c745fa83073..81db85f5bb07bc9949f3e7316fd10b605359df51 100644 (file)
--- 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 $<