diff options
-rw-r--r-- | doc/ci/jenkins/index.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/ci/jenkins/index.md b/doc/ci/jenkins/index.md index 9ec10f2e694..093b3568a78 100644 --- a/doc/ci/jenkins/index.md +++ b/doc/ci/jenkins/index.md @@ -1,6 +1,6 @@ --- comments: false -type: index +type: index, howto --- # Migrating from Jenkins |