Skip to content

Fix indentation, add output in documentation #100

Fix indentation, add output in documentation

Fix indentation, add output in documentation #100

Workflow file for this run

name: "pre-release"
on:
push:
branches:
- main
env:
IDRIS2_TESTS_CG: jvm
ACTIONS_ALLOW_UNSECURE_COMMANDS: true
PREVIOUS_VERSION: 0.6.0.11
jobs:
pre-release:
name: "Pre Release"
runs-on: "ubuntu-latest"
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Set up JDK 8
uses: actions/setup-java@v2
with:
java-version: '8'
distribution: 'adopt'
cache: 'maven'
server-id: ossrh
server-username: MAVEN_USERNAME
server-password: MAVEN_PASSWORD
gpg-private-key: ${{ secrets.GPG_PRIVATE_KEY }}
gpg-passphrase: GPG_PASSPHRASE
- name: Set IDRIS2_PREFIX
run: echo IDRIS2_PREFIX="$HOME/bin/idris2-$PREVIOUS_VERSION/env" >> "$GITHUB_ENV"
- name: Set PREFIX
run: echo PREFIX="$IDRIS2_PREFIX" >> "$GITHUB_ENV"
- name: Download previous version
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"
- name: Publish to Maven Central
run: mvn -B -Prelease deploy
env:
MAVEN_USERNAME: ${{ secrets.OSSRH_USERNAME }}
MAVEN_PASSWORD: ${{ secrets.OSSRH_PASSWORD }}
GPG_PASSPHRASE: ${{ secrets.GPG_PASSPHRASE }}
- name: Publish to Github
uses: "marvinpinto/action-automatic-releases@latest"
with:
repo_token: "${{ secrets.GITHUB_TOKEN }}"
automatic_release_tag: development
prerelease: true
title: "Development Build"
files: |
idris-jvm-compiler/target/idris2-*.zip