diff options
Diffstat (limited to 'tools/check-translate')
| -rwxr-xr-x | tools/check-translate | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/check-translate b/tools/check-translate index 3dd82405..acb6f459 100755 --- a/tools/check-translate +++ b/tools/check-translate @@ -2,7 +2,7 @@ echo -------------- Producing translated files --------------------- rm */*/*.v8 >& /dev/null -make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; } +make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; } if [ -e translated ]; then rm -r translated; fi if [ -e successful-translation ]; then rm -r successful-translation; fi if [ -e failed-translation ]; then rm -r failed-translation; fi |