Document `rand_weighted()` in Random number generation #1581

	name: Continuous integration

	on:
	push:
	pull_request:

	concurrency:
	group: ${{ github.workflow }}-${{ github.event.pull_request.number \|\| github.ref }}
	cancel-in-progress: true

	jobs:
	build:
	runs-on: ubuntu-22.04
	steps:
	- name: Checkout
	uses: actions/checkout@v4

	- name: Install dependencies
	run: \|
	# Install tools used by `_tools/format.sh`.
	sudo apt-get -qq update
	sudo apt-get -qq install dos2unix recode
	sudo pip3 install -r requirements.txt
	sudo pip3 install codespell

	- name: Linter checks
	run: \|
	bash _tools/format.sh

	codespell -D- -D _tools/codespell-dict.txt -I _tools/codespell-ignore.txt -x _tools/codespell-ignore-lines.txt -S tutorials/i18n/locales.rst {about,community,contributing,getting_started,tutorials}/{.rst,/.rst,//.rst,///.rst}

	# Use dummy builder to improve performance as we don't need the generated HTML in this workflow.
	- name: Sphinx build
	run: make SPHINXOPTS='--color -W' dummy

Provide feedback