@@ -13,12 +13,22 @@ if not "GITLAB_TOKEN" in os.environ:
...
@@ -13,12 +13,22 @@ if not "GITLAB_TOKEN" in os.environ:
print("You can create such tokens at <https://gitlab.mpi-sws.org/profile/personal_access_tokens>.")
print("You can create such tokens at <https://gitlab.mpi-sws.org/profile/personal_access_tokens>.")
print("Make sure you grant access to the 'api' scope.")
print("Make sure you grant access to the 'api' scope.")
sys.exit(1)
sys.exit(1)
ifnot"IRIS_REV"inos.environ:
print("Please set IRIS_REV, STDPP_REV, ORC11_REV and GPFSL_REV environment variables to the branch/tag/commit of the respective project that you want to use.")
print("Only IRIS_REV is mandatory, the rest defaults to 'master'.")