Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added redirect.html
authorhaftmann
Tue, 04 Oct 2005 14:58:44 +0200
changeset 17752 a92cda068ad8
parent 17751 2cc8429943f2
child 17753 f84b032417ac
added redirect.html
Admin/website/build/make_dep.bash file | annotate | diff | comparison | revisions
Admin/website/build/set_perm.bash file | annotate | diff | comparison | revisions
Admin/website/redirect.html file | annotate | diff | comparison | revisions 
--- 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"
--- 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
--- /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 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+    <title>Isabelle</title>
+    <?include file="//include/htmlheader.include.html"?>
+    <meta content="0; URL=http://isabelle.in.tum.de/" http-equiv="refresh" />
+</head>
+
+<body class="main">
+    <?include file="//include/header.include.html"?>
+    <div class="hr"><hr/></div>
+
+    <div id="content">
+        <h2>Redirect</h2>
+        <p>Please visit the Isabelle project page at <a shape="rect" href="http://isabelle.in.tum.de/">http://isabelle.in.tum.de/</a>.</p>
+    </div>
+
+    <div class="hr"><hr/></div>
+    <?include file="//include/footer.include.html"?>
+</body>
+
+</html>
isabelle