diff options
| author | Matthieu Sozeau | 2014-08-26 14:58:47 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-26 14:58:47 +0200 |
| commit | 9ef5dbb1f340971036aa0c7d4d7a0986188fd971 (patch) | |
| tree | 39a7980164a5127a0ab7e39b5e5c625a1d16daa6 /dev/include | |
| parent | bbcb802d81fad79fc76bde031bafb130132946ba (diff) | |
Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors in
stm test-suite files.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions