diff options
| author | Gaëtan Gilbert | 2019-07-08 13:07:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-08 13:07:30 +0200 |
| commit | a5e4dd7faa23abd4a4ebe093076484d090a8a47e (patch) | |
| tree | e0de245adb468dc3fe95d9108be749f010457365 /dev | |
| parent | 5ecfe31f9d900c6053531f2cb713035407009ba7 (diff) | |
| parent | 07abf9818a6b47bb2c2bd0a8201da9743a0c10b6 (diff) | |
Merge PR #9686: [error] Remove special error printing pre-processing
Reviewed-by: SkySkimmer
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index b30bbaa3fa..4841db8953 100644 --- a/dev/base_include +++ b/dev/base_include @@ -134,7 +134,6 @@ open Tacticals open Tactics open Eqschemes -open ExplainErr open Class open ComDefinition open Indschemes |