fix sorting for n equal m (#246) #173
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: Publish Dev Docs | |
on: | |
push: | |
branches: | |
- main | |
jobs: | |
publish: | |
runs-on: ubuntu-latest | |
steps: | |
- name: Checkout repository | |
uses: actions/checkout@v4 | |
with: | |
fetch-depth: 0 | |
- name: Setup packages | |
uses: ./.github/actions/setup | |
- name: Install dependencies | |
run: | | |
pip install -e .[doc] | |
- name: Get variables | |
run: | | |
python -c 'import pathpyG; print(f"package_version={pathpyG.__version__}")' >> "$GITHUB_ENV" | |
echo "sha_short=$(git rev-parse --short "$GITHUB_SHA")" >> "$GITHUB_ENV" | |
- name: Publish docs | |
# First configure git correctly | |
# Then use the alias of the current dev version to delete it based on its identifier | |
# Then deploy the new version so that there is only one dev version at a time | |
run: | | |
git config user.name github-actions | |
git config user.email [email protected] | |
git fetch origin gh-pages --depth=1 | |
mike delete --push $(mike list | grep dev | awk '{print $1}' | tr -d '()') | |
mike deploy --push --update-aliases "${{ env.package_version }}-dev" dev | |
mike set-default --push --allow-empty dev |