GitLab

Thanks to the previous commit of @mikael-s.

Useful so that make doesn't tell it has failed while it was just the file that
already existed

See !147

See #3003.

See #3003.

'make demo' should be run before this

See #2635.

Follows #3003.
Re-closes #3032.

We add '-X 1000' to command lines on LIL-L4.
See #3027.

Closes #3032.

out/ directory may not exist, leading to errors.
In that case we can do without temporary files.

When calling exit() the memory allocated by the system is not
properly free-ed. This is not really a problem in itself but
Valgrind will complain about that.

There are two solutions:
1. replace exit() with return, but this
   requires to be in the main() function
2. prevent Valgrind from being used in
   other cases (exit because of an error)

See #3031

Some allocations were not properly free-ed.
Spotted by Valgrind.

See #3031

See #3031

See #2247.

Closes #3003.

See #3003.

See #3003.

Closes #2635.

See #2635.

See #2635.

See #2635, but also #3027.

See #2635.

Closes #3012 and opens #3026.

The {} initializer was buggy on some g++-4.8 versions.

Closes #3023