---
doc/Makefile.local | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/doc/Makefile.local b/doc/Makefile.local
index bab3d0d2..dfe62295 100644
--- a/doc/Makefile.local
+++ b/doc/Makefile.local
@@ -56,7 +56,7 @@ sphinx-texinfo:
$(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS)
David Mazieres writes:
> Dan Čermák writes:
>
>> Could you maybe elaborate in more detail, as I don't know how it would
>> help me exactly? Are you running a server for syncing your tags?
>>
>> My problem is the following: I have 3 machines E, B and C of which none
>> is always up and running. I