diff options
Diffstat (limited to 'utils/clflags.mli')
| -rw-r--r-- | utils/clflags.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/utils/clflags.mli b/utils/clflags.mli index 5d9cb86312..8cab8f15ac 100644 --- a/utils/clflags.mli +++ b/utils/clflags.mli @@ -189,7 +189,6 @@ val dlcode : bool ref val pic_code : bool ref val runtime_variant : string ref val with_runtime : bool ref -val force_tmc : bool ref val force_slash : bool ref val keep_docs : bool ref val keep_locs : bool ref |