Remove Github mention from CI badges docs

diff --git a/src/doc/book/src/reference/manifest.md b/src/doc/book/src/reference/manifest.md
index 6a2fdc5f27f0018a4f3a3f806a194b8fa7abb1ba..6a79c7a1bac438f38c3285f759a4d065f5f7821f 100644 (file)
--- a/src/doc/book/src/reference/manifest.md
+++ b/src/doc/book/src/reference/manifest.md
@@ -188,7 +188,7 @@ license-file = "..."
 #   which state the issue resolution time, percent of open issues, and future
 #   maintenance intentions.
 #
-# If a `repository` key is required, this refers to a Github repository in
+# If a `repository` key is required, this refers to a repository in
 # `user/repo` format.
 [badges]
 

diff --git a/src/doc/manifest.md b/src/doc/manifest.md
index 2650a516d282b8a092308eedb7b9082788986541..4a72712d2231ca123ded2c7fea02a8f69f7696b8 100644 (file)
--- a/src/doc/manifest.md
+++ b/src/doc/manifest.md
@@ -185,7 +185,7 @@ license-file = "..."
 #   which state the issue resolution time, percent of open issues, and future
 #   maintenance intentions.
 #
-# If a `repository` key is required, this refers to a Github repository in
+# If a `repository` key is required, this refers to a repository in
 # `user/repo` format.
 [badges]