aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-08-26 14:58:47 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-08-26 14:58:47 +0200
commit9ef5dbb1f340971036aa0c7d4d7a0986188fd971 (patch)
tree39a7980164a5127a0ab7e39b5e5c625a1d16daa6 /tactics
parentbbcb802d81fad79fc76bde031bafb130132946ba (diff)
Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors in
stm test-suite files.
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions