Skip to content

Update dockerfile

Update dockerfile #3

Workflow file for this run

name: ci-in-docker
on:
push:
branches:
- master
pull_request:
workflow_dispatch:
jobs:
docker:
runs-on: ubuntu-latest
steps:
- run: echo "🎉 The job was automatically triggered by a ${{ github.event_name }} event."
- run: echo "🐧 This job is now running on a ${{ runner.os }} server hosted by GitHub!"
- run: echo "🔎 The name of your branch is ${{ github.ref }} and your repository is ${{ github.repository }}."
- run: echo "The user is $USER"
- run: cat /etc/issue
- name: Check out repository code
uses: actions/checkout@v4
- run: echo "💡 The ${{ github.repository }} repository has been cloned to the runner."
- run: echo "🖥️ The workflow is now ready to test your code on the runner."
- name: List files in the repository
run: |
ls ${{ github.workspace }}
- run: echo "Build Docker image"
- run: make docker-build
- run: echo "Build paper.pdf in Docker container"
- run: make docker-paper.pdf
- run: echo "🍏 This job's status is ${{ job.status }}."