CI: Fix license check on empty diffs in [scripts/lint.sh]

What

Fixes the license check in scripts/lint.sh to handle cases where diff \ exclude_patterns is empty.

Why

The license check uses grep -v to remove all patterns in $exclude_patterns from the set of files in $diff. However, grep -v fails if no lines are selected.

This will happen when e.g. "$diff" is empty. This may happen since diff only contains the set of new files that are in:

source_directories=(src docs/doc_gen tezt devtools contrib etherlink)

(like in this diff: !12118 (diffs) ... all of the files are in source_directories but none of them are new).

It can also happen if "$diff \ $exclude_patterns" is empty (that is, when all of the changed files are in the exclude_patterns).

How

It is OK that no lines are selected, therefore we append || true to this line.

Manually testing the MR

Try this with / without the patch:

$ git checkout sribaroud@etherlink@fix_docker_command
$ CI_MERGE_REQUEST_DIFF_BASE_SHA=$(git merge-base HEAD origin/master) ./scripts/ci/lint_check_licenses.sh

Checklist

• Document the interface of any function added or modified (see the coding guidelines)
• Document any change to the user interface, including configuration parameters (see node configuration)
• Provide automatic testing (see the testing guide).
• For new features and bug fixes, add an item in the appropriate changelog (docs/protocols/alpha.rst for the protocol and the environment, CHANGES.rst at the root of the repository for everything else).
• Select suitable reviewers using the Reviewers field below.
• Select as Assignee the next person who should take action on that MR