Remove unused import from pipes

Also, the module "pipes" is no longer available with Python 3.13.
hso-praktomat · Oct 16, 2024 · 9fb5bbd · 9fb5bbd
1 parent 35711fc
commit 9fb5bbd
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 3 deletions.
diff --git a/src/checker/checker/IsabelleChecker.py b/src/checker/checker/IsabelleChecker.py
@@ -1,4 +1,3 @@
-from pipes import quote
 import shutil, os, re, subprocess
 from django.conf import settings
 

diff --git a/src/checker/checker/RChecker.py b/src/checker/checker/RChecker.py
@@ -1,4 +1,3 @@
-from pipes import quote
 import shutil, os, re, subprocess
 from django.conf import settings
 

diff --git a/src/checker/compiler/Builder.py b/src/checker/compiler/Builder.py
@@ -1,5 +1,4 @@
 import os
-from pipes import quote
 import re, subprocess
 import shlex
 from django.db import models