Remove outdated entry in gitignore

polypheny · May 5, 2024 · 72c08ea · 72c08ea
1 parent 1b3d820
commit 72c08ea
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/.gitignore b/.gitignore
@@ -253,6 +253,3 @@ nbdist/
 
 # Ignore dynamically generated version file
 src/main/resources/version.properties
-
-# Ignoreproto files
-src/main/proto/