Remove outdated make server target

goblint · Feb 19, 2024 · cc3c733 · cc3c733
1 parent ebcf24a
commit cc3c733
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/make.sh b/make.sh
@@ -140,9 +140,6 @@ rule() {
       ./scripts/update_suite.rb # run regression tests
     ;; testci)
       ruby scripts/update_suite.rb -s -d # -s: run tests sequentially instead of in parallel such that output is not scrambled, -d shows some stats?
-    ;; server)
-      rsync -avz --delete --exclude='/.git' --exclude='server.sh' --exclude-from="$(git ls-files --exclude-standard -oi --directory > /tmp/excludes; echo /tmp/excludes)" . serverseidl6.informatik.tu-muenchen.de:~/analyzer2
-      ssh serverseidl6.informatik.tu-muenchen.de 'cd ~/analyzer2; make nat && make test'
 
     ;; *)
       echo "Unknown action '$1'. Try clean, native, byte, profile or doc.";;