Don't keep rebuilding the PO files. Have a separate 'update-po' rule.

diff --git a/Makefile.in b/Makefile.in
index 799da69..35582d1 100644 (file)
--- a/Makefile.in
+++ b/Makefile.in
@@ -50,7 +50,7 @@ endif
 TARGETS                = $(MANPAGES) $(TEXTMANPAGES)
 
 all: $(TARGETS)
-       for d in $(SUBDIRS); do \
+       for d in $(SUBDIRS_NOT_PO); do \
          $(MAKE) -C $$d $@; \
          if [ $$? -ne 0 ]; then exit 1; fi; \
        done
@@ -83,6 +83,11 @@ distclean: clean
        rm -f Makefile
        rm -f */Makefile
 
+# Rebuild the PO files.
+
+update-po:
+       $(MAKE) -C po all
+
 # Developer documentation (in html/ subdirectory).
 
 ifneq ($(OCAMLDOC),)