diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 02:41:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-22 14:39:31 +0100 |
| commit | e8419bac30ab98527ec6b15d5a0f5c1035539ca5 (patch) | |
| tree | a9e2766e23ccb0afac63edac44f4442a92686501 /kernel | |
| parent | fa3a97426013cf940cd25abde43c0191766218b1 (diff) | |
[library] Remove `-boot` option.
The `-boot` option was used to:
- suppress loading of the rc_file
- allow to save modules with prefix `Coq`
There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.
Fixes: #9575
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions