[CI] Change docker lint message

[gigiblender]

This PR changes the docker lint error message.

@areusch

cc @Mousius @driazati

[github-actions]

Built docs for commit 9fa414294066b069162c5e80d625e0fb92c84293 can be found here.

[leandron]

Hi @gigiblender - thanks for the PR. While I acknowledge you fix is very simple and shouldn't do any harm to the code base, I don't think the usage of the [skip ci] here applies within the agreed rules.

The reason is that this PR is not fixing a blocking issue in CI, which is the intention of the [skip ci] mechanism to exist. For this reason, could you please update the header of this PR and re-trigger CI, so that we can then merge it?

For reference, here is[skip ci] header description:

tvm/jenkins/README.md

Lines 76 to 84 in b9890db

	## Skipping CI
	For reverts and trivial forward fixes, adding `[skip ci]` to the revert's
	PR title will cause CI to shortcut and only run lint. Committers should
	take care that they only merge CI-skipped PRs to fix a failure on `main` and
	not in cases where the submitter wants to shortcut CI to merge a change faster.
	The PR title is checked when the build is first run (specifically during the lint
	step, so changes after that has run do not affect CI and will require the job to
	be re-triggered by another `git push`).

[leandron]

cc @driazati

[github-actions]

Built docs for commit 9fa414294066b069162c5e80d625e0fb92c84293 can be found here.

[gigiblender]

Hi @gigiblender - thanks for the PR. While I acknowledge you fix is very simple and shouldn't do any harm to the code base, I don't think the usage of the [skip ci] here applies within the agreed rules.

The reason is that this PR is not fixing a blocking issue in CI, which is the intention of the [skip ci] mechanism to exist. For this reason, could you please update the header of this PR and re-trigger CI, so that we can then merge it?

For reference, here is[skip ci] header description:

tvm/jenkins/README.md

Lines 76 to 84 in b9890db

	## Skipping CI
	For reverts and trivial forward fixes, adding `[skip ci]` to the revert's
	PR title will cause CI to shortcut and only run lint. Committers should
	take care that they only merge CI-skipped PRs to fix a failure on `main` and
	not in cases where the submitter wants to shortcut CI to merge a change faster.
	The PR title is checked when the build is first run (specifically during the lint
	step, so changes after that has run do not affect CI and will require the job to
	be re-triggered by another `git push`).

Apologies @leandron. Wasn't aware of that. I changed the title and reran the CI.

[areusch]

thanks @gigiblender , @leandron can you approve?

[leandron]

LGTM, thanks!