CI: added workflow_dispatch to docker jobs

.github/workflows/docker.yml

@@ -7,6 +7,7 @@ on:
   pull_request:
     branches:
       - '**'
+  workflow_dispatch:
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
@@ -22,8 +23,9 @@ jobs:
     #    $ sudo apt-get upgrade qemu-user-static
     #    $ docker run --rm --privileged multiarch/qemu-user-static --reset -p yes -c yes
     # More info: https://github.com/introlab/rtabmap/issues/1454
-    # Skipped on pull requests; built and pushed only on push to master.
-    if: github.event_name != 'pull_request'
+    # Skipped on pull requests; built and pushed only from master (push or
+    # manual dispatch), since it pushes the :*-deps tags to Docker Hub.
+    if: github.ref == 'refs/heads/master'
 
     runs-on: ubuntu-latest
     
@@ -101,7 +103,8 @@ jobs:
   docker:
     needs: docker_deps
     # Run even when docker_deps is skipped (it is, on pull requests).
-    if: ${{ !cancelled() && !failure() }}
+    # A manual dispatch is honored only on master, the only ref we push from.
+    if: ${{ !cancelled() && !failure() && (github.event_name != 'workflow_dispatch' || github.ref == 'refs/heads/master') }}
     runs-on: ubuntu-latest
     
     strategy: