Docs: fix build filter, update push branch (#745)

Author: droserasprout

.github/workflows/docs.yml

@@ -18,7 +18,7 @@ on:
       - '.github/workflows/docs.yml'
 
 env:
-  FRONTEND_BRANCH: actual-docs
+  FRONTEND_BRANCH: master
   GH_TOKEN: ${{ secrets.API_TOKEN_EXT }}
 
 jobs:
@@ -59,6 +59,7 @@ jobs:
         run: pdm run docs_build
 
       - name: Commit and push frontend
+        if: github.ref == 'refs/heads/next'
         run: |
           cd ../interface
           git config --local user.email "[email protected]"

docs/1.getting-started/2.core-concepts.md

@@ -4,7 +4,7 @@ description: "Before proceeding to development, let's take a look at basic DipDu
 ---
 
 # Core concepts
-
+ 
 Before proceeding to development, let's take a look at basic DipDup concepts. The main terms are highlighted in _italics_ and will be discussed in detail in the following sections.
 
 ## Big picture

scripts/docs.py

@@ -61,8 +61,8 @@ def on_modified(self, event: FileSystemEvent) -> None:
             return
 
         # FIXME: front dies otherwise
-        # if not (src_file.name[0] == '_' or src_file.name[0].isdigit()):
-        #     return
+        if not (src_file.name[0] == '_' or src_file.name[0].isdigit()):
+            return
 
         if event.event_type == EVENT_TYPE_DELETED:
             dst_file = (self._destination / src_file.relative_to(self._source)).resolve()