Files
coursebook/_scripts
Lawrence Angrave c688b2dd43 Deploy with the built-in GITHUB_TOKEN instead of deploy keys
Every deploy has been failing at the push with "git@github.com:
Permission denied (publickey)". The repo has no deploy keys registered
at all, so the keys inside site-deploy.enc and wiki-deploy.enc cannot
authenticate - most likely lost in the illinois-cs241 ->
cs341-illinois org rename. GPG decryption itself still works, so
GPG_PASSPHRASE is not the problem.

Comment out the gpg/ssh-agent machinery and push over https with the
built-in GITHUB_TOKEN, granting the job contents: write. Nothing to
rotate, and it survives future renames.

site_deploy.sh stays disabled: it pushes to a different repo to nudge
the website into rebuilding, which GITHUB_TOKEN cannot do, and it still
names the twice-stale illinois-cs241/illinois-cs241.github.io.
2026-08-23 22:01:35 -05:00
..
2018-11-09 16:50:16 -06:00
2019-07-23 12:45:36 -05:00
2023-12-18 14:42:15 -06:00
2019-07-23 10:53:37 -05:00
2019-07-23 14:20:57 -05:00

Scripts

  • __init__.py Init to make a python package
  • deploy.sh Script to run in travis deploy stage
  • script.sh Script to run in travis script stages
  • install.sh Script to run in travis install stage
  • gen_order.py Generates the latex order file from the yaml file
  • gen_wiki.py Generates a wiki given an order file and output directory
  • pandoc_header_filter.py Outputs a yaml block to stderr given the metadata of the file
  • pandoc_wiki_filter.py Filters a latex wiki page with additional add ons
  • push_to_wiki.sh Script to run in the push to wiki stage
  • site_cleanup.sh Script to clean up pushing to the site
  • site_deploy.sh Script to deploy to the site
  • site_retry.sh Script to retry