refactor

.github/workflows/on commit.yaml

@@ -1,64 +1,16 @@
 name: Pack and test
 
 on:
+#    push:
     schedule:
         - cron: '0 0 * * *'
     pull_request:
     workflow_dispatch:
-
-#concurrency:
-#    group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
-#    cancel-in-progress: false
-#    
+
 permissions:
     contents: write
-    
+
 jobs:
-    update-gh-pages:
-        runs-on: ubuntu-latest
-
-        steps:
-            - uses: actions/checkout@main
-
-            - run: |
-            
-                git config --global core.autocrlf false
-                git config --global user.name "sun pack bot"
-                git config --global user.email "[email protected]"
-                git config --global --add url.https://github.com/.insteadOf "[email protected]:"
-                git fetch origin
-                
-                for branch in $(git branch -r | grep 'origin/gh-pages/'); do
-                    branch_name=$(echo $branch | sed 's#origin/gh-pages/##')
-                    echo "Testing legacy branch [$branch]"
-                    
-                    if ! git branch -r | grep -q "origin/$branch_name"; then
-                        echo "Deleting legacy branch [$branch]"
-                        git push origin --delete $(echo $branch | sed 's#origin/##')
-                    fi
-                    
-                done
-                
-                branch_name="gh-pages/$(git rev-parse --abbrev-ref HEAD)"
-                git checkout --orphan "$branch_name"
-                mv ".git" "Packing/Reference/0Release/"
-                cd "Packing/Reference/0Release/"
-                git add .
-                git commit -m "Split off gh-pages"
-                
-                if git show-ref --verify --quiet refs/remotes/origin/$branch_name; then
-                    echo "Remote branch $branch_name found"
-                    if [ -z "$( git diff "origin/$branch_name" )" ]; then
-                        echo "No difference with remote branch"
-                        exit 0
-                    else
-                        echo "Difference found, recreating the branch"
-                    fi
-                else
-                    echo "Creating new remote branch"
-                fi
-                git push -f --set-upstream origin "$branch_name"
-                
     pack-win:
         runs-on: windows-latest
 

.github/workflows/update gh-pages.yaml

@@ -0,0 +1,55 @@
+name: Pack and test
+
+on:
+    push:
+    workflow_dispatch:
+
+permissions:
+    contents: write
+
+jobs:
+    update-gh-pages:
+        runs-on: ubuntu-latest
+
+        steps:
+            - uses: actions/checkout@main
+
+            - run: |
+            
+                git config --global core.autocrlf false
+                git config --global user.name "sun pack bot"
+                git config --global user.email "[email protected]"
+                git config --global --add url.https://github.com/.insteadOf "[email protected]:"
+                git fetch origin
+                
+                for branch in $(git branch -r | grep 'origin/gh-pages/'); do
+                    branch_name=$(echo $branch | sed 's#origin/gh-pages/##')
+                    echo "Testing legacy branch [$branch]"
+                    
+                    if ! git branch -r | grep -q "origin/$branch_name"; then
+                        echo "Deleting legacy branch [$branch]"
+                        git push origin --delete $(echo $branch | sed 's#origin/##')
+                    fi
+                    
+                done
+                
+                branch_name="gh-pages/$(git rev-parse --abbrev-ref HEAD)"
+                git checkout --orphan "$branch_name"
+                mv ".git" "Packing/Reference/0Release/"
+                cd "Packing/Reference/0Release/"
+                git add .
+                git commit -m "Split off gh-pages"
+                
+                if git show-ref --verify --quiet refs/remotes/origin/$branch_name; then
+                    echo "Remote branch $branch_name found"
+                    if [ -z "$( git diff "origin/$branch_name" )" ]; then
+                        echo "No difference with remote branch"
+                        exit 0
+                    else
+                        echo "Difference found, recreating the branch"
+                    fi
+                else
+                    echo "Creating new remote branch"
+                fi
+                git push -f --set-upstream origin "$branch_name"
+                

.github/workflows/upstream pretest.yaml

@@ -5,42 +5,61 @@ on:
     schedule:
         - cron: '0 0 * * *'
     workflow_dispatch:
-
-#concurrency:
-#    group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
-#    cancel-in-progress: false
-#    
+
 permissions:
     contents: write
-    
+
 jobs:
     enmr-PRs:
         runs-on: windows-latest
 
         steps:
-            - uses: actions/checkout@main
+            - name: git config
+                run: |
+                
+                    git config --global core.autocrlf false
+                    git config --global --add url.https://github.com/.insteadOf "[email protected]:"
             
-            - run: |
+            - name: checkout
+                uses: actions/checkout@main
+                sparse-checkout-cone-mode: false
+                sparse-checkout: |
+                  .gitmodules
             
-                git config --global core.autocrlf false
-                git config --global user.name "sun pack bot"
-                git config --global user.email "[email protected]"
-                git config --global --add url.https://github.com/.insteadOf "[email protected]:"
+            - name: make exec list
+                run: |
                 
-                git submodule update --init --recursive
-                
-                Write-Host (git submodule --quiet foreach 'echo $path').Length
-                Write-Host (git submodule --quiet foreach 'echo $path' 2>1).Length
-                git submodule --quiet foreach 'echo $path'
+                    foreach ($subm_key in git config --file .gitmodules --name-only --get-regexp '^submodule\..+\.url$') {
+                        $subm_url = git config --file .gitmodules --get $subm_key
+                        
+                        Write-Host "URL: $subm_url"
+                        
+                        foreach ($ref_l in git ls-remote $remote_url 'refs/pull/*/merge') {
+                            if ($ref_l -notmatch '^[0-9a-f]+\s+refs/pull/(\d+)/merge$') {
+                                throw "Unexpected format: $ref_l"
+                            }
+                            
+                            $pr_num = $Matches[1]
+                            
+                            Write-Host "- Found PR $pr_num"
+                        }
+                        
+                    }
+            
+    pretest-each:
+        runs-on: windows-latest
+
+        steps:
+            - name: git config
+                run: |
                 
-                foreach ($subm_path in git submodule --quiet foreach 'echo $path') {
-                    Write-Host $subm_path
-                    Push-Location $subm_path
-                    
-                    git config --add remote.origin.fetch "+refs/pull/*/merge:refs/remotes/origin/pr/*"
-                    
-                    git fetch --dry-run origin
-                    
-                    Pop-Location
-                }
-                
+                    git config --global core.autocrlf false
+                    git config --global user.name "sun pack bot"
+                    git config --global user.email "[email protected]"
+            
+            - name: checkout
+                uses: actions/checkout@main
+                with:
+                    submodules: 'true'
+                    token: ${{ secrets.PAT_TOKEN }}
+