CD integration for uploading to HotCRP#85
Conversation
bollu
left a comment
bollu
left a comment
There was a problem hiding this comment.
If I understand correctly, I can use 'upload-to-hotcrp.sh' without adding it as a GH action, correct? Very sweet.
While I'm not the biggest fan of shell scripts, this one is well written (too well written 🤖) so LGTM.
| local name="$1" | ||
| local value="${!name:-}" | ||
|
|
||
| if [ -z "$value" ] || [ "$value" = "TODO" ] || [ "$value" = "TODO_REPLACE_ME" ]; then |
There was a problem hiding this comment.
| if [ -z "$value" ] || [ "$value" = "TODO" ] || [ "$value" = "TODO_REPLACE_ME" ]; then | |
| if [ -z "$value" ] || [ "$value" = "TODO" ]; then |
Do we really need to check for two different todo values?
There was a problem hiding this comment.
we now check for all the TODO values
| CONFIG_FILE is sourced as a shell env file. If omitted, .github/hotcrp.env is | ||
| sourced when it exists; otherwise existing environment variables are used. |
There was a problem hiding this comment.
Is this actually accurate w.r.t what's implemented?
not the biggest fan either, but we don't really want to bloat the actions container with other packages, right? |
I mean, since you already use python, and the main point of this script is to just send a HTTP request (right?), why not just use python for all of it? I guess there is a little bloat / startup time then if you want to use the python's request library (I assume you'd have to install it via pip or something). You could fix that via some caching of the pip modules, but that's probably over-engineering. Yeah, I guess if a shell script works it's probably the simplest solution |
3 participants
This PR adds an opt-in script to
toolsthat uploadssubmisison.pdfto HotCRP in GitHub Actions.