.github/workflows/tox-optional.yml: Rename

Matthias Koeppe · Matthias Koeppe · commit 84edb00974f4 · 2020-04-18T12:11:30.000-07:00
diff --git a/.github/workflows/tox-optional.yml b/.github/workflows/tox-optional.yml
@@ -1,4 +1,4 @@
-name: Run SAGE_ROOT/tox.ini
+name: Run SAGE_ROOT/tox.ini TARGETS_OPTIONAL
 
 ## This GitHub Actions workflow runs SAGE_ROOT/tox.ini with select environments,
 ## whenever a GitHub pull request is opened or synchronized in a repository

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-name: Run SAGE_ROOT/tox.ini`
	`1`	`+name: Run SAGE_ROOT/tox.ini TARGETS_OPTIONAL`
`2`	`2`
`3`	`3`	`## This GitHub Actions workflow runs SAGE_ROOT/tox.ini with select environments,`
`4`	`4`	`## whenever a GitHub pull request is opened or synchronized in a repository`