Correction of default_value
type in UniformFloatHyperparameter
and UniformIntegerHyperparameter
#431
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: docs | |
on: | |
# Trigger manually | |
workflow_dispatch: | |
# Trigger on any push to the main | |
push: | |
branches: | |
- main | |
- development | |
# Trigger on any push to a PR that targets main | |
pull_request: | |
branches: | |
- main | |
- development | |
permissions: | |
contents: write | |
env: | |
name: "ConfigSpace" | |
jobs: | |
build-and-deploy: | |
runs-on: ubuntu-latest | |
steps: | |
- name: Checkout | |
uses: actions/checkout@v3 | |
- name: Setup Python | |
uses: actions/setup-python@v3 | |
with: | |
python-version: "3.8" | |
- name: Install dependencies | |
run: | | |
pip install build | |
pip install ".[docs]" | |
- name: Make docs | |
run: | | |
make clean | |
make docs | |
- name: Pull latest gh-pages | |
if: (contains(github.ref, 'develop') || contains(github.ref, 'main')) && github.event_name == 'push' | |
run: | | |
cd .. | |
git clone https://github.com/${{ github.repository }}.git --branch gh-pages --single-branch gh-pages | |
- name: Copy new docs into gh-pages | |
if: (contains(github.ref, 'develop') || contains(github.ref, 'main')) && github.event_name == 'push' | |
run: | | |
branch_name=${GITHUB_REF##*/} | |
cd ../gh-pages | |
rm -rf $branch_name | |
cp -r ../${{ env.name }}/docs/build/html $branch_name | |
- name: Push to gh-pages | |
if: (contains(github.ref, 'develop') || contains(github.ref, 'main')) && github.event_name == 'push' | |
run: | | |
last_commit=$(git log --pretty=format:"%an: %s") | |
cd ../gh-pages | |
branch_name=${GITHUB_REF##*/} | |
git add $branch_name/ | |
git config --global user.name 'Github Actions' | |
git config --global user.email '[email protected]' | |
git remote set-url origin https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/${{ github.repository }} | |
git commit -am "$last_commit" | |
git push |