diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2019-03-30 17:42:13 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2019-03-30 17:42:13 -0400 |
| commit | 8e561ed471518c426c59f210f5ea07d4f178cbe5 (patch) | |
| tree | 65882d8388bac00b96168bfce279943638a54453 /src/settings.sml | |
| parent | d51f7f2770858713204b7e670119090a26c9f194 (diff) | |
Ensure compilation fails even if the only problem is a missing source file
Diffstat (limited to 'src/settings.sml')
0 files changed, 0 insertions, 0 deletions