From da61874293fdcf7c22117d3f2d1022d3981a1862 Mon Sep 17 00:00:00 2001
From: partain <unknown>
Date: Mon, 22 Jan 1996 18:59:42 +0000
Subject: [PATCH] [project @ 1996-01-22 18:59:42 by partain] Add -no-hi-diffs
flag (from dnt)
---
ghc/driver/ghc.lprl | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/ghc/driver/ghc.lprl b/ghc/driver/ghc.lprl
index 7f00cd2f8f7d..8ccef55cfca9 100644
--- a/ghc/driver/ghc.lprl
+++ b/ghc/driver/ghc.lprl
@@ -601,8 +601,9 @@ arg: while($_ = $ARGV[0]) {
/^-nohi$/ && do { $ProduceHi = 0; next arg; };
# don't generate an interface (even if generating C)
- /^-hi-diffs$/ && do { $HiDiff_flag = 1; next arg; };
- # show diffs if the interface file changes
+ /^-hi-diffs$/ && do { $HiDiff_flag = 1; next arg; };
+ /^-no-hi-diffs$/ && do { $HiDiff_flag = 0; next arg; };
+ # show/disable diffs if the interface file changes
/^-E$/ && do { push(@CcBoth_flags, '-E');
$Only_preprocess_C = 1;
--
GitLab