Skip to content

Commit

Permalink
fix mike
Browse files Browse the repository at this point in the history
  • Loading branch information
RexWzh committed Aug 5, 2024
1 parent d65def2 commit aefe71a
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 13 deletions.
23 changes: 18 additions & 5 deletions .github/workflows/preview.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,9 @@ on:
pull_request:
branches:
- main
push:
branches:
- preview
permissions:
contents: write
pull-requests: write
Expand All @@ -28,7 +31,8 @@ jobs:
mkdocs-material-
- run: pip install -r requirements.txt
- run: |
mike deploy dev -p
git fetch origin
mike deploy dev -p --allow-empty
echo "Preview URL: https://leanprover.cn/dev/" >> $GITHUB_STEP_SUMMARY
- name: Comment PR with Preview Link
Expand All @@ -37,10 +41,19 @@ jobs:
script: |
const { payload } = context;
const prNumber = payload.number;
const previewLink = `https://leanprover.cn/dev/`;
github.rest.issues.createComment({
const baseUrl = 'https://leanprover.cn';
const previewLink = `${baseUrl}/dev/`;
const comments = await github.rest.issues.listComments({
issue_number: prNumber,
owner: context.repo.owner,
repo: context.repo.repo,
body: `Preview available at: ${previewLink}`
});
});
const existingComment = comments.data.find(comment => comment.body.includes(previewLink));
if (!existingComment) {
await github.rest.issues.createComment({
issue_number: prNumber,
owner: context.repo.owner,
repo: context.repo.repo,
body: `Preview available at: ${previewLink}`
});
}
9 changes: 1 addition & 8 deletions docs/assets/css/custom.css
Original file line number Diff line number Diff line change
Expand Up @@ -10,18 +10,11 @@ body {
}

.md-content img {
max-width: 200px;
max-width: 75%;
display: block;
margin: 0 auto;
}

.md-content blockquote {
font-style: italic;
color: #555;
border-left: 4px solid #8bc34a;
padding-left: 15px;
margin-left: 0;
}

.md-content p {
margin-top: 20px;
Expand Down

0 comments on commit aefe71a

Please sign in to comment.