Publish Website/Guide #82

	name: Publish Website/Guide

	# Controls when the workflow will run
	on:
	push:
	branches:
	- master
	# Allows you to run this workflow manually from the Actions tab
	workflow_dispatch:

	jobs:
	build-deploy-guide:
	# Only run on `MLton` organization
	if: github.repository_owner == 'MLton'

	# The type of runner that the job will run on
	runs-on: ubuntu-latest

	# Steps represent a sequence of tasks that will be executed as part of the job
	steps:
	# Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
	- name: Checkout
	uses: actions/checkout@v4
	with:
	fetch-depth: 0

	- name: Setup SSH
	run: ./.github/scripts/setup_ssh.sh
	env:
	SSH_KEY_RSA: ${{ secrets.MLTON_WEBMASTER_SSH_KEY_RSA }}
	SSH_KEY_ED25519: ${{ secrets.MLTON_WEBMASTER_SSH_KEY_ED25519 }}
	SSH_CONFIG: ${{ secrets.MLTON_WEBMASTER_SSH_CONFIG }}
	SSH_KNOWN_HOSTS: ${{ secrets.MLTON_WEBMASTER_SSH_KNOWN_HOSTS }}

	- name: Install guide dependencies
	uses: ./.github/actions/install-guide-dependencies

	- name: Build
	run: make -j 2 -C doc/guide mlton.sourceforge.io

	- name: Deploy
	run: make -C doc/guide MLTON_SOURCEFORGE_IO_USER=mlton-webmaster upload_mlton.sourceforge.io

Provide feedback