diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rwxr-xr-x | dev/tools/update-compat.py | 2 |
2 files changed, 1 insertions, 2 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 diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index 0338cd42c7..c7bb36b6d3 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +#!/usr/bin/env python2 from __future__ import with_statement import os, re, sys, subprocess |