diff options
| author | Ralf Jung <post@ralfj.de> | 2019-07-23 10:50:45 +0200 |
|---|---|---|
| committer | Who? Me?! <mark-i-m@users.noreply.github.com> | 2019-07-23 15:36:51 -0500 |
| commit | 92d432a0c710dfabf507de24ab95e491dc6a7449 (patch) | |
| tree | fc1248a51605b20c1ea300cb661c170be664b24c /src/tools/publish_toolstate.py | |
| parent | 9c48ed4eab3d2f6050803479f76db0aafecdd7c7 (diff) | |
| download | rust-92d432a0c710dfabf507de24ab95e491dc6a7449.tar.gz rust-92d432a0c710dfabf507de24ab95e491dc6a7449.zip | |
more callback docs
Diffstat (limited to 'src/tools/publish_toolstate.py')
| -rwxr-xr-x | src/tools/publish_toolstate.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/tools/publish_toolstate.py b/src/tools/publish_toolstate.py index 8f9061d7c18..0f1ae5e0eb2 100755 --- a/src/tools/publish_toolstate.py +++ b/src/tools/publish_toolstate.py @@ -1,6 +1,9 @@ #!/usr/bin/env python # -*- coding: utf-8 -*- +## This is set as callback for `src/ci/docker/x86_64-gnu-tools/repo.sh` by the CI scripts +## when a new commit lands on `master` (i.e., after it passed all checks on `auto`). + import sys import re import os |