From 41ddf9c50e932b99ca49a57c5042f827d28dde29 Mon Sep 17 00:00:00 2001 From: Francois Kritzinger Date: Tue, 29 Oct 2024 09:02:15 +0200 Subject: Doc fixes --- doc/manual.cli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/manual.cli') diff --git a/doc/manual.cli b/doc/manual.cli index 678b497..7ae8ca3 100644 --- a/doc/manual.cli +++ b/doc/manual.cli @@ -683,7 +683,7 @@ GitHub supports integration of third-party CI services into the repository workflow by allowing such third-party services to register for events (called \i{web hooks} in the GitHub terminology). -\N|This mechanism should not be confused with GitHub Actions, with is a GitHub +\N|This mechanism should not be confused with GitHub Actions, which is a GitHub built-in CI service. As far as we understand, it uses ad hoc integration rather than the same integration mechanism as available to third-party CI services.| @@ -758,7 +758,7 @@ PR does not get invalidated (because the PR head hasn't changed). Let's consider two representative examples of each case that show how the GitHub behavior can lead us to making wrong decisions. But before we do that, -last bit of terminology: we will distinguish between \i{local PRs}, those with +a last bit of terminology: we will distinguish between \i{local PRs}, those with the head branch from the same repository, and \i{remote PRs}, those with the head branch belonging to another user/organization (called \i{forked PR} in the GitHub terminology). -- cgit v1.1