Update KNI-tutorial repository #26

	---
	name: Update KNI-tutorial repository
	on:
	workflow_dispatch:
	jobs:
	update-repo:
	runs-on: ubuntu-latest
	permissions:
	contents: write # To push a branch
	steps:
	- name: Checkout Khiops sources
	uses: actions/checkout@v3
	with:
	path: khiops
	- name: Put Khiops version on the environment
	run: echo "KHIOPS_VERSION=$(./khiops/scripts/khiops-version)" >> "$GITHUB_ENV"
	- name: Checkout KNI-tutorial
	uses: actions/checkout@v3
	with:
	repository: KhiopsML/KNI-tutorial
	ssh-key: ${{ secrets.KNI_TUTORIAL_SSH_KEY }}
	path: tutorial
	# Copy sources files and README.md from khiops repository to KNI-tutorial
	# README.md and *.c files are generated by cmake configure
	- name: Update local KNI-tutorial
	run: \|
	cmake -B khiops/build -S khiops -DMPI=OFF -DBUILD_JARS=OFF -DBUILD_LEX_YACC=OFF -DTESTING=OFF
	cp khiops/build/tmp/kni.README.md tutorial/README.md
	cp khiops/build/tmp/KNIRecodeFile.c tutorial/cpp/
	cp khiops/build/tmp/KNIRecodeMTFiles.c tutorial/cpp/
	cp khiops/src/Learning/KhiopsNativeInterface/KhiopsNativeInterface.h tutorial/include/
	cp khiops/src/Learning/KNITransfer/KNIRecodeFile.h tutorial/cpp/
	cp khiops/src/Learning/KNITransfer/KNIRecodeMTFiles.h tutorial/cpp/
	- name: Update remote KNI-tutorial
	run: \|-
	cd tutorial
	git config --global user.email "[email protected]"
	git config --global user.name "khiops bot"
	git commit -am"update to v${{ env.KHIOPS_VERSION }}"
	git push
	git tag ${{ env.KHIOPS_VERSION }}
	git push --tags

Provide feedback