Assignments will now run in Docker when pull requests are created. If I create a pull request from foo/serg-andy to SERG-Delft/andy, then the assignments will be run, in Docker, on the HEAD of the head repository (here: foo/serg-andy). Pushes remain unaffected, the assignments will run, in Docker, on the HEAD of what is pushed.
Refactored the pipeline a bit to facilitate this.
Fixed a bug where assignments would not run if your fork's name is not andy.
Removed assignments_test.py as it is no longer used (and suffers from the above bug), in consultation with @martinmladenov.
The comments self-explanatory, if you have any questions, let me know. Surprisingly, there is no way to set the [directory] option when cloning in the checkout action (the Python script needs the repository location). This is poor design on behalf of GitHub actions, and I work around this by injecting the repository name excluding the owner alongside the commit hash.
This encompasses:
foo/serg-andy
toSERG-Delft/andy
, then the assignments will be run, in Docker, on theHEAD
of the head repository (here:foo/serg-andy
). Pushes remain unaffected, the assignments will run, in Docker, on theHEAD
of what is pushed.andy
.assignments_test.py
as it is no longer used (and suffers from the above bug), in consultation with @martinmladenov.The comments self-explanatory, if you have any questions, let me know. Surprisingly, there is no way to set the
[directory]
option when cloning in the checkout action (the Python script needs the repository location). This is poor design on behalf of GitHub actions, and I work around this by injecting the repository name excluding the owner alongside the commit hash.Closes #220.