Fix the header-lint job rucio#4980

The `header-lint` job of the github actions reports "You have divergent
branches". This is a side effect of pulling the master branch into an already
checked-out repository. Since we have not specified the merge strategy, the job
fails.

We do not need to pull the master branch directly, since the `checkout` github
action automatically pulls the entire history for **all** branches. [1]

This commit removes the pull of the master branch, thus

[1] https://github.com/actions/checkout#fetch-all-history-for-all-tags-and-branches

.github/workflows/autotest.yml

@@ -15,7 +15,6 @@ jobs:
       - name: Check headers
         shell: bash
         run: |
-          git pull origin master
           echo "Current git rev $(git rev-parse HEAD)"
           echo "Common ancestor git rev $(git merge-base HEAD remotes/origin/master)"
           echo "If a file header needs to be changed run 'tools/add_header -i FILE' from the rucio project directory."