Automatically delete source/Makefile.dep if remaking fails

git-svn-id: https://svn.dealii.org/trunk@22681 0785d39b-7218-0410-832d-ea1e28bc413d

diff --git a/deal.II/Makefile b/deal.II/Makefile
index 87f378608f2d5a0e391f4c3c065d331644e23393..f664001b4dbb6b493c7a9a72091f88a5e5cff388 100644 (file)
--- a/deal.II/Makefile
+++ b/deal.II/Makefile
@@ -2,6 +2,7 @@
 #
 # Makefile for the whole library
 
+SHELL=/bin/bash
 
 help:
        @echo "========================================================================"
@@ -25,7 +26,9 @@ help:
 
 deps:
        cd common/scripts && $(MAKE) $(MAKEOPTIONS)
-       cd source && $(MAKE) $(MAKEOPTIONS) Makefile.dep
+       @cd source && if $(MAKE) $(MAKEOPTIONS) Makefile.dep;\
+         then echo > /dev/null ;\
+         else rm Makefile.dep && $(MAKE) $(MAKEOPTIONS) Makefile.dep; fi
        cd lib && $(MAKE) $(MAKEOPTIONS) external-links