add handle for custom device (#61) #56

	name: Benchmarks

	on:
	push:
	branches: devel

	jobs:

	Benchmark:

	runs-on: ubuntu-latest
	if: github.repository == 'pyccel/pyccel'

	steps:
	- name: Set up ssh
	uses: webfactory/[email protected]
	with:
	ssh-private-key: ${{ secrets.SSH_DEPLOY_KEY }}
	- name: Clone pyccel-benchmarks repository
	working-directory: ../
	run: \|
	git clone [email protected]:pyccel/pyccel-benchmarks.git
	- name: Push results to pyccel-benchmarks
	working-directory: ../pyccel-benchmarks
	run: \|
	export GIT_AUTHOR_NAME="Pyccel/pyccel"
	export GIT_AUTHOR_EMAIL="41898282+github-actions[bot]@users.noreply.github.com"
	git config user.email ${GIT_AUTHOR_EMAIL}
	git config user.name ${GIT_AUTHOR_NAME}
	git commit --allow-empty -m "Benchmark of pyccel/pyccel@${GITHUB_SHA}"
	git push

Provide feedback