Bug 518265: Papyrus-RT HIPP excessive disk usage

Pre-build script to periodically clean the local Maven repo.

https://bugs.eclipse.org/bugs/show_bug.cgi?id=518265

Change-Id: I2159d03774ee00eeb91352e4d215fe1613db4441

1 files changed, 53 insertions, 3 deletions

diff --git a/releng/scripts/prebuild.sh b/releng/scripts/prebuild.sh
index c5b233d51..5546020cf 100644
--- a/releng/scripts/prebuild.sh
+++ b/releng/scripts/prebuild.sh
@@ -1,6 +1,5 @@
 #--------------------------------------------------------------------------------
-# Copyright (c) 2012-2016 CEA LIST.
-#
+# Copyright (c) 2012, 2017 CEA LIST, Christian W. Damus, and others.
 #    
 # All rights reserved. This program and the accompanying materials
 # are made available under the terms of the Eclipse Public License v1.0
@@ -8,10 +7,61 @@
 # http://www.eclipse.org/legal/epl-v10.html
 #
 # Contributors:
-#	 Celine Janssens (All4Tec)
+#	 Celine Janssens (All4Tec) - Initial API and implementation
+#    Christian W. Damus - bug 518265
 #--------------------------------------------------------------------------------
 
 #!/bin/sh
+set -eux
+
+PRIVATE_MAVEN="$WORKSPACE/.maven"
+PRIVATE_REPO="$PRIVATE_MAVEN/repo"
+LAST_CLEANED_RECORD="$PRIVATE_MAVEN/.lastCleaned"
+TODAY=`date "+%Y-%m-%d"`
+
+#
+# Function determining whether the private Maven repository should be cleaned.
+#
+need_clean_repo() {
+	if [[ ! -f "$LAST_CLEANED_RECORD" ]]; then
+		return 0; # Initial clean to be recorded
+	fi
+	
+	# The first word of the record is the build ID that was cleaned
+	# The rest of the record is the date that it was cleaned
+	read lastCleanedBuild lastCleanedDate < "$LAST_CLEANED_RECORD"
+	
+	# Clean if the last cleaned build was ten builds ago
+	if (( "$BUILD_NUMBER" - "$lastCleanedBuild" >= 10 )); then
+		# But only if that was not today
+		if [[ "$lastCleanedDate" == "$TODAY" ]]; then
+			return 1
+		fi
+		
+		return 0
+	fi
+	
+	# No need to clean
+	return 1
+}
+
+#
+# Function to clean the private maven repository.
+#
+clean_repo() {
+	rm -rf "$PRIVATE_REPO"
+	mkdir -p "$PRIVATE_REPO"
+	echo "$BUILD_NUMBER $TODAY" > "$LAST_CLEANED_RECORD"
+}
+
+# Clean the Maven repository if it's time
+if need_clean_repo; then
+	clean_repo
+fi
+
+if [[ -z "$LOCAL_REPO_DIR" ]]; then
+	LOCAL_REPO_DIR = "$WORKSPACE/source"
+fi
 
 cd $LOCAL_REPO_DIR
 git clean -fdx