]> https://gitweb.dealii.org/ - dealii.git/commitdiff
Automatically delete source/Makefile.dep if remaking fails
authorGuido Kanschat <dr.guido.kanschat@gmail.com>
Wed, 10 Nov 2010 16:17:23 +0000 (16:17 +0000)
committerGuido Kanschat <dr.guido.kanschat@gmail.com>
Wed, 10 Nov 2010 16:17:23 +0000 (16:17 +0000)
git-svn-id: https://svn.dealii.org/trunk@22681 0785d39b-7218-0410-832d-ea1e28bc413d

deal.II/Makefile

index 87f378608f2d5a0e391f4c3c065d331644e23393..f664001b4dbb6b493c7a9a72091f88a5e5cff388 100644 (file)
@@ -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
 
 

In the beginning the Universe was created. This has made a lot of people very angry and has been widely regarded as a bad move.

Douglas Adams


Typeset in Trocchi and Trocchi Bold Sans Serif.