change tld #182
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI | |
| on: | |
| push: | |
| branches: [ master ] | |
| pull_request: | |
| branches: [ master ] | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v2 | |
| - name: Cache Racket dependencies | |
| uses: actions/cache@v2 | |
| with: | |
| path: | | |
| ~/.cache/racket | |
| ~/.local/share/racket | |
| key: default | |
| - name: Install Racket | |
| uses: Bogdanp/[email protected] | |
| with: | |
| architecture: 'x64' | |
| distribution: 'full' | |
| version: '7.9' | |
| packages: 'gregor,frog,honu' | |
| #- name: Setup upterm session | |
| # uses: lhotari/action-upterm@v1 | |
| - name: Build website | |
| run: | | |
| sudo apt-get install -y python3-pygments | |
| sudo make all | |
| - name: Deploy website | |
| if: ${{ github.event_name == 'push' }} | |
| run: | | |
| sudo git config --global user.name "github-actions[bot]" | |
| sudo git config --global user.email "nuprl+github-actions[bot]@users.noreply.github.com" | |
| sudo git add -A -f | |
| sudo git checkout -b "deploy" | |
| sudo git commit --allow-empty -m "** deploy nuprl/website@$GITHUB_SHA" | |
| sudo git push origin deploy -f |