git: Rename some directory.

This commit is contained in:
Pierre-Antoine Rouby committed 2023-03-30 09:29:33 +02:00
1 parent b8dd88f4fd
commit d418b57fa0
138 files changed
+40 -41

No files matched your search

+3
View File
@@ -0,0 +1,3 @@
# -*- coding: utf-8 -*-
solver_type_list = ["generic"]