Skip to content

Commit

Permalink
Fix ubuntu self host build, linter errors
Browse files Browse the repository at this point in the history
  • Loading branch information
mmhelloworld committed Apr 2, 2024
1 parent a165e85 commit 0d80e45
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions .github/workflows/install.yml
Original file line number Diff line number Diff line change
Expand Up @@ -38,21 +38,21 @@ jobs:
run: |
mvn dependency:copy "-Dartifact=io.github.mmhelloworld:idris-jvm-compiler:$PREVIOUS_VERSION:zip" -DoutputDirectory=. -U
unzip idris-jvm-compiler-*.zip -d "$HOME/bin"
echo "::add-path::$HOME/bin/idris2-$PREVIOUS_VERSION/exec"
echo "$HOME/bin/idris2-$PREVIOUS_VERSION/exec" >> "$GITHUB_PATH"
- name: Build
run: mvn -B install -Dinteractive= -Didris.tests=only=jvm

- name: Copy new version
run: |
mkdir -p "$HOME/bin/idris2-current"
cp -rf build/exec "$HOME/bin/idris2-current/exec"
cp -rf build/env "$HOME/bin/idris2-current/env"
unzip idris-jvm-compiler/target/idris2-*.zip -d "$HOME/bin/idris2-current"
- name: Use new version
run: |
echo "::add-path::$HOME/bin/idris2-current/exec"
echo IDRIS2_PREFIX="$HOME/bin/idris2-current/env" >> "$GITHUB_ENV"
NEW_VERSION=$(mvn help:evaluate -Dexpression=project.version -q -DforceStdout)
echo "$HOME/bin/idris2-current/idris2-$NEW_VERSION/exec" >> "$GITHUB_PATH"
echo IDRIS2_PREFIX="$HOME/bin/idris2-current/idris2-$NEW_VERSION/env" >> "$GITHUB_ENV"
echo PREFIX="$IDRIS2_PREFIX" >> "$GITHUB_ENV"
- name: Self host
Expand Down Expand Up @@ -96,7 +96,7 @@ jobs:
run: |
mvn dependency:copy "-Dartifact=io.github.mmhelloworld:idris-jvm-compiler:$PREVIOUS_VERSION:zip" -DoutputDirectory=. -U
unzip idris-jvm-compiler-*.zip -d "$HOME/bin"
echo "::add-path::$HOME/bin/idris2-$PREVIOUS_VERSION/exec"
echo "$HOME/bin/idris2-$PREVIOUS_VERSION/exec" >> $GITHUB_PATH
- name: Build
run: mvn -B install -Dinteractive= -Didris.tests=only=jvm
Expand All @@ -109,7 +109,7 @@ jobs:
- name: Use new version
run: |
echo "::add-path::$HOME/bin/idris2-current/exec"
echo "$HOME/bin/idris2-current/exec" >> $GITHUB_PATH
echo IDRIS2_PREFIX="$HOME/bin/idris2-current/env" >> "$GITHUB_ENV"
echo PREFIX="$IDRIS2_PREFIX" >> "$GITHUB_ENV"
Expand Down

0 comments on commit 0d80e45

Please sign in to comment.