# HG changeset patch # User haftmann # Date 1128430724 -7200 # Node ID a92cda068ad88f160d99f39446c4213ee62ee46f # Parent 2cc8429943f245a675c7b71a27aa2be5277a1638 added redirect.html diff -r 2cc8429943f2 -r a92cda068ad8 Admin/website/build/make_dep.bash --- a/Admin/website/build/make_dep.bash Tue Oct 04 14:37:06 2005 +0200 +++ b/Admin/website/build/make_dep.bash Tue Oct 04 14:58:44 2005 +0200 @@ -23,7 +23,7 @@ echo ' mkdir -p $(dir $@)' >> "$DEP_FILE" echo ' -chmod $(TARGET_UMASK_DIR) $(dir $@)' >> "$DEP_FILE" echo ' -chgrp $(TARGET_GROUP) $(dir $@)' >> "$DEP_FILE" - echo ' rm $@' >> "$DEP_FILE" + echo ' -[ -e $@ ] && rm $@' >> "$DEP_FILE" echo ' cp $< $@' >> "$DEP_FILE" echo ' chmod $(TARGET_UMASK_DIR) $@' >> "$DEP_FILE" echo ' chgrp $(TARGET_GROUP) $@' >> "$DEP_FILE" @@ -43,7 +43,7 @@ echo ' mkdir -p $(dir $@)' >> "$DEP_FILE" echo ' -chmod $(TARGET_UMASK_DIR) $(dir $@)' >> "$DEP_FILE" echo ' -chgrp $(TARGET_GROUP) $(dir $@)' >> "$DEP_FILE" - echo ' rm $@' >> "$DEP_FILE" + echo ' -[ -e $@ ] && rm $@' >> "$DEP_FILE" echo ' $(PYTHON) build/pypager.py --dtd="dtd/" $(FORCE_ENC_CMD) --srcroot="." --dstroot="$(OUTPUTROOT)" distname="$(DISTNAME)" $< $@' >> "$DEP_FILE" echo ' -$(TIDYCMD) $@' >> "$DEP_FILE" echo ' chmod $(TARGET_UMASK_DIR) $@' >> "$DEP_FILE" diff -r 2cc8429943f2 -r a92cda068ad8 Admin/website/build/set_perm.bash --- a/Admin/website/build/set_perm.bash Tue Oct 04 14:37:06 2005 +0200 +++ b/Admin/website/build/set_perm.bash Tue Oct 04 14:58:44 2005 +0200 @@ -25,5 +25,6 @@ chmod "$LOCAL_UMASK_FILE" "$file" fi fi + chgrp "$LOCAL_GROUP" "$file" fi done diff -r 2cc8429943f2 -r a92cda068ad8 Admin/website/redirect.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/website/redirect.html Tue Oct 04 14:58:44 2005 +0200 @@ -0,0 +1,25 @@ + + + + + + + Isabelle + + + + + + +
+ +
+

Redirect

+

Please visit the Isabelle project page at http://isabelle.in.tum.de/.

+
+ +
+ + + +