Pulse: error on binder attributes, they are ignored #1955

	name: CI

	on:
	push:
	branches-ignore:
	- _**
	pull_request:
	workflow_dispatch:
	merge_group:

	defaults:
	run:
	shell: bash

	jobs:
	# opam and nix builds run on a nightly schedule, see nightly-ci.yml.
	# It is a bit excessive to run them on every push.

	ci:
	runs-on: ubuntu-latest
	container: mtzguido/dev-base:v2
	steps:
	- name: Cleanup
	run: sudo find . -delete
	- run: echo "HOME=/home/user" >> $GITHUB_ENV
	- uses: mtzguido/set-opam-env@master

	- uses: actions/checkout@master
	with:
	path: FStar
	submodules: true

	- name: Run CI
	run: make -skj$(nproc) ci
	working-directory: FStar

	# Branch protection points here
	ciok:
	runs-on: ubuntu-latest
	if: ${{ cancelled() \|\| contains(needs..result, 'cancelled') \|\| contains(needs..result, 'failure') }}
	# ^ Workaround for insane github behavior: https://github.com/actions/runner/issues/2566
	needs:
	- ci
	steps:
	# Note: we only run on failure. Otherwise this is skipped, which counts
	# as a success.
	- run: exit 1

Provide feedback