diff options
| author | Björn Gustavsson <[email protected]> | 2017-11-03 11:02:53 +0100 |
|---|---|---|
| committer | Björn Gustavsson <[email protected]> | 2017-11-06 15:43:56 +0100 |
| commit | cfb75380fcba60058825815068eac8e402d10e40 (patch) | |
| tree | 008efaa3187412f5713ea71f2a1530a4bcd6c2e9 /.gitignore | |
| parent | 0c88933a6ea89250460532847529699774a60b2a (diff) | |
| download | otp-cfb75380fcba60058825815068eac8e402d10e40.tar.gz otp-cfb75380fcba60058825815068eac8e402d10e40.tar.bz2 otp-cfb75380fcba60058825815068eac8e402d10e40.zip | |
Warn when $REFRESH_GEN_DEST() is not used after a GC
It is easy to to forget to use $REFRESH_GEN_DEST() in an instruction
that has a general destionation ('d'). Add a heuristic that should
catch most if not all such problems.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions