Merge pull request #629 from kevinzakka:github-action-change

PiperOrigin-RevId: 494105265 Change-Id: Idaad9a69ba54b280e34fbebe4e47497ba822137c
2022-12-09 01:04:18 -08:00
parent 91455b3e1e d7e082ae96
commit 064d9f9707
1 changed files with 4 additions and 0 deletions
@@ -11,8 +11,12 @@ name: build
 on:
  push:
    branches: [main]
+    paths-ignore:
+      - "doc/**"
  pull_request:
    branches: [main]
+    paths-ignore:
+      - "doc/**"

 jobs:
  mujoco: