JETLS.jl/.github/workflows/Documentation.yml at f98b05496092a5e92a421c7175d0fdaef6eef5b3 · aviatesk/JETLS.jl · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
name: Documentation

on:
  push:
    branches:
      - master
    paths:
      - "docs/**"
      - "CHANGELOG.md"
      - ".github/workflows/Documentation.yml"
  pull_request:
    paths:
      - "docs/**"
      - "CHANGELOG.md"
      - ".github/workflows/Documentation.yml"

jobs:
  build:
    # These permissions are needed to:
    # - Deploy the documentation: https://documenter.juliadocs.org/stable/man/hosting/#Permissions
    # - Delete old caches: https://github.com/julia-actions/cache#usage
    permissions:
      actions: write
      contents: write
      pull-requests: read
      statuses: write
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: julia-actions/setup-julia@v2
        with:
          version: '1'
      - uses: julia-actions/cache@v2
      - name: Install dependencies
        shell: julia --color=yes --project=docs {0}
        run: |
          using Pkg
          Pkg.develop(PackageSpec(path=pwd()))
          Pkg.instantiate()
      - name: Get release date
        id: release_date
        run: |
          # Fetch release branch to get the latest release date
          git fetch origin release --depth=100
          DATE=$(git log origin/release --oneline --grep="^release:" -1 --format="%s" | grep -oE '[0-9]{4}-[0-9]{2}-[0-9]{2}' || echo "")
          echo "date=$DATE" >> $GITHUB_OUTPUT
      - name: Build and deploy
        run: julia --color=yes --project=docs docs/make.jl
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
          DOCUMENTER_KEY: ${{ secrets.DOCUMENTER_KEY }}
          DOCUMENTER_RELEASE_DATE: ${{ steps.release_date.outputs.date }}
      - name: Set release as default version
        if: github.event_name == 'push'
        run: |
          git config user.name "github-actions[bot]"
          git config user.email "github-actions[bot]@users.noreply.github.com"
          git stash --include-untracked
          git fetch origin gh-pages
          git checkout gh-pages
          # Create redirect pages for each directory under release/
          for item in release/*/; do
            name=$(basename "$item")
            [ -d "$name" ] && continue  # Skip if already exists (e.g., dev, previews)
            mkdir -p "$name"
            cat > "$name/index.html" << EOF
          <!DOCTYPE html>
          <html>
          <head>
            <script>window.location.href = "/JETLS.jl/release/$name/" + window.location.hash;</script>
            <noscript><meta http-equiv="refresh" content="0; url=/JETLS.jl/release/$name/"></noscript>
          </head>
          </html>
          EOF
          done
          # Root redirect
          cat > index.html << 'EOF'
          <!DOCTYPE html>
          <html>
          <head>
            <script>window.location.href = "/JETLS.jl/release/" + window.location.hash;</script>
            <noscript><meta http-equiv="refresh" content="0; url=/JETLS.jl/release/"></noscript>
          </head>
          </html>
          EOF
          git add -A
          git diff --staged --quiet || git commit -m "Update root redirects to release content"
          git push origin gh-pages