Skip to content

Merge branch 'develop' into develop #2

Merge branch 'develop' into develop

Merge branch 'develop' into develop #2

Workflow file for this run

# Simple workflow for deploying static content to GitHub Pages
name: Deploy eBPF hub Pages
on:
# Runs on pushes targeting the develop branch
push:
branches:
- "develop"
paths:
- 'eBPF_Hub/**'
- 'lib/**'
- '.github/workflows/eBPF_hub.yml'
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
contents: read
pages: write
id-token: write
# Allow one concurrent deployment
concurrency:
group: "pages"
cancel-in-progress: true
# In that case do the job 'make_and_deploy_doxygen'
jobs:
deploy:
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
- name: get submodule
run: git submodule update --init --recursive
- name: install deps
run: |
sudo make -C lib/build_hub install-deps
- name: build compile set
run: |
make -C lib/build_hub clone_and_install_deps
make -C lib/build_hub test
- name: Build with Jekyll
uses: actions/jekyll-build-pages@v1
with:
source: ./eBPF_Hub
destination: ./_site
- name: Setup Pages
uses: actions/configure-pages@v1
- name: Upload artifact
uses: actions/upload-pages-artifact@v1
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@main