add 'corepin' flag

diff --git a/Robust/src/buildscript b/Robust/src/buildscript
index 9fc8b98bb3913703c1e940776d15923a98c98109..12c75a561df4b560cef7d7ac8191caf83c440373 100755 (executable)
--- a/Robust/src/buildscript
+++ b/Robust/src/buildscript
@@ -369,6 +369,9 @@ EXTRAOPTIONS="$EXTRAOPTIONS -DMAC"
 elif [[ $1 = '-squeue' ]]
 then
 EXTRAOPTIONS="$EXTRAOPTIONS -DSQUEUE"
+elif [[ $1 = '-corepin' ]]
+then
+EXTRAOPTIONS="$EXTRAOPTIONS -DCOREPIN"
 SQUEUE=true
 elif [[ $1 = '-profile' ]]
 then