diff options
Diffstat (limited to 'test-suite')
24 files changed, 500 insertions, 35 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index c0bdb29fab..c60f39231e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -32,18 +32,21 @@ include ../Makefile.common # Variables ####################################################################### -# Default value when called from a freshly compiled Coq, but can be -# easily overridden - +ifneq ($(wildcard ../_build),) +BIN:=$(shell cd ..; pwd)/_build/install/default/bin/ +COQLIB:=$(shell cd ..; pwd)/_build/install/default/lib/coq +else BIN := $(shell cd ..; pwd)/bin/ -COQFLAGS?= COQLIB?= ifeq ($(COQLIB),) COQLIB := $(shell ocaml ocaml_pwd.ml ..) endif +endif # exists ../_build export COQLIB +COQFLAGS?= + coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -R prerequisite TestSuite coqdoc := $(BIN)coqdoc diff --git a/test-suite/bugs/closed/bug_10669.v b/test-suite/bugs/closed/bug_10669.v new file mode 100644 index 0000000000..433e300acb --- /dev/null +++ b/test-suite/bugs/closed/bug_10669.v @@ -0,0 +1,12 @@ + +Context (A0:Type) (B0:A0). +Definition foo0 := B0. + +Set Universe Polymorphism. +Context (A1:Type) (B1:A1). +Definition foo1 := B1. + +Section S. + Context (A2:Type) (B2:A2). + Definition foo2 := B2. +End S. diff --git a/test-suite/bugs/closed/bug_10888.v b/test-suite/bugs/closed/bug_10888.v new file mode 100644 index 0000000000..3c2e8011d7 --- /dev/null +++ b/test-suite/bugs/closed/bug_10888.v @@ -0,0 +1,11 @@ + +Module Type T. +Context {A:Type}. +End T. + +Module M(X:T). + Import X. + Check X.A. + Check A. + Definition B := A. +End M. diff --git a/test-suite/bugs/closed/bug_10894.v b/test-suite/bugs/closed/bug_10894.v new file mode 100644 index 0000000000..b8c9367951 --- /dev/null +++ b/test-suite/bugs/closed/bug_10894.v @@ -0,0 +1,12 @@ +(* Check that uconstrs are interpreted in the ltac-substituted environment *) +(* Was a regression introduced in 4dab4fc (#7288) *) + +Tactic Notation "bind" hyp(x) "in" uconstr(f) "as" ident(h) := + set (h := fun x => f). + +Fact test : nat -> nat. +Proof. + intros n. + bind n in (n*n) as f. + assert (f 0 = 0) by reflexivity. +Abort. diff --git a/test-suite/bugs/closed/bug_10904.v b/test-suite/bugs/closed/bug_10904.v new file mode 100644 index 0000000000..32b25ff726 --- /dev/null +++ b/test-suite/bugs/closed/bug_10904.v @@ -0,0 +1,8 @@ +Definition a := fun (P:SProp) (p:P) => p. + +Lemma foo : (let k := a in let k' := a in fun (x:nat) y => x) = (let k := a in fun x y => y). +Proof. + Fail reflexivity. + match goal with |- ?l = _ => exact_no_check (eq_refl l) end. +Fail Qed. +Abort. diff --git a/test-suite/bugs/closed/bug_6323.v b/test-suite/bugs/closed/bug_6323.v index fdc33befc6..24feb7155c 100644 --- a/test-suite/bugs/closed/bug_6323.v +++ b/test-suite/bugs/closed/bug_6323.v @@ -6,4 +6,5 @@ Goal True. simple refine (let id' : { x : X' | True } -> X' := _ in _); [ abstract refine (@proj1_sig _ _) | ] ]. -Abort. + exact I. +Defined. diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v new file mode 100644 index 0000000000..25285622a9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9512.v @@ -0,0 +1,35 @@ +Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia. + +Set Primitive Projections. +Record params := { width : Z }. +Definition p : params := Build_params 64. + +Set Printing All. + +Goal width p = 0%Z -> width p = 0%Z. + intros. + + assert_succeeds (enough True; [omega|]). + assert_succeeds (enough True; [lia|]). + +(* H : @eq Z (width p) Z0 *) +(* ============================ *) +(* @eq Z (width p) Z0 *) + + change tt with tt in H. + +(* H : @eq Z (width p) Z0 *) +(* ============================ *) +(* @eq Z (width p) Z0 *) + + assert_succeeds (enough True; [lia|]). + (* Tactic failure: <tactic closure> fails. *) + (* assert_succeeds (enough True; [omega|]). *) + (* Tactic failure: <tactic closure> fails. *) + + (* omega. *) + (* Error: Omega can't solve this system *) + + lia. + (* Tactic failure: Cannot find witness. *) +Qed. diff --git a/test-suite/bugs/closed/bug_9851.v b/test-suite/bugs/closed/bug_9851.v new file mode 100644 index 0000000000..1f57ce8471 --- /dev/null +++ b/test-suite/bugs/closed/bug_9851.v @@ -0,0 +1,18 @@ +Require Import Ring_base. +Record word : Type := Build_word + { rep : Type; + zero : rep; one: rep; + add : rep -> rep -> rep; + sub : rep -> rep -> rep; + opp : rep -> rep; + mul : rep -> rep -> rep; + }. +Axiom rth + : forall (word : word ), + @ring_theory (@rep word) + (@zero word) + (@one word) (@add word) + (@mul word) (@sub word) + (@opp word) (@eq (@rep word)). + +Fail Add Ring wring: (@rth _). diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v index 820022d995..27cb731151 100644 --- a/test-suite/bugs/opened/bug_1596.v +++ b/test-suite/bugs/opened/bug_1596.v @@ -69,9 +69,8 @@ Definition t := (X.t * Y.t)%type. elim (X.lt_not_eq H2 H3). elim H0;clear H0;intros. right. - split. - eauto. - eauto. + split; + eauto with ordered_type. Qed. Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). @@ -97,7 +96,7 @@ Definition t := (X.t * Y.t)%type. apply EQ. split;trivial. apply GT. - right;auto. + right;auto with ordered_type. apply GT. left;trivial. Defined. diff --git a/test-suite/ltac2/ltac2env.v b/test-suite/ltac2/ltac2env.v new file mode 100644 index 0000000000..743e62932d --- /dev/null +++ b/test-suite/ltac2/ltac2env.v @@ -0,0 +1,15 @@ +Require Import Ltac2.Ltac2. + +Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end. + +Goal True. +Proof. +(* Fails at runtime because not fully applied *) +Fail ltac1:(ltac2:(x |- ())). +(* Type mismatch: Ltac1.t vs. constr *) +Fail ltac1:(ltac2:(x |- pose $x)). +(* Check that runtime cast is OK *) +ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t nat). +(* Type mismatch *) +Fail ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t ident:(foo)). +Abort. diff --git a/test-suite/misc/votour.sh b/test-suite/misc/votour.sh new file mode 100755 index 0000000000..ac26aed49b --- /dev/null +++ b/test-suite/misc/votour.sh @@ -0,0 +1,3 @@ +command -v "${BIN}votour" || { echo "Missing votour"; exit 1; } + +"${BIN}votour" prerequisite/ssr_mini_mathcomp.vo < /dev/null diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out new file mode 100644 index 0000000000..9ca3fa3357 --- /dev/null +++ b/test-suite/output-coqtop/DependentEvars.out @@ -0,0 +1,91 @@ + +Coq < +Coq < Coq < 1 subgoal + + ============================ + forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R + +(dependent evars: ; in current goal:) + +strange_imp_trans < +strange_imp_trans < No more subgoals. + +(dependent evars: ; in current goal:) + +strange_imp_trans < +Coq < Coq < 1 subgoal + + ============================ + forall P Q : Prop, (P -> Q) /\ P -> Q + +(dependent evars: ; in current goal:) + +modpon < +modpon < No more subgoals. + +(dependent evars: ; in current goal:) + +modpon < +Coq < Coq < +Coq < P1 is declared +P2 is declared +P3 is declared +P4 is declared + +Coq < p12 is declared + +Coq < p123 is declared + +Coq < p34 is declared + +Coq < Coq < 1 subgoal + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + P4 + +(dependent evars: ; in current goal:) + +p14 < +p14 < 4 focused subgoals +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?Q -> P4 + +subgoal 2 is: + ?P -> ?Q +subgoal 3 is: + ?P -> ?Q +subgoal 4 is: + ?P + +(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5) + +p14 < 3 focused subgoals +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?P -> (?Goal2 -> P4) /\ ?Goal2 + +subgoal 2 is: + ?P -> (?Goal2 -> P4) /\ ?Goal2 +subgoal 3 is: + ?P + +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11) + +p14 < +Coq < +Coq < diff --git a/test-suite/output-coqtop/DependentEvars.v b/test-suite/output-coqtop/DependentEvars.v new file mode 100644 index 0000000000..5a59054073 --- /dev/null +++ b/test-suite/output-coqtop/DependentEvars.v @@ -0,0 +1,24 @@ +Set Printing Dependent Evars Line. +Lemma strange_imp_trans : + forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R. +Proof. + auto. +Qed. + +Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q. +Proof. + tauto. +Qed. + +Section eex. + Variables P1 P2 P3 P4 : Prop. + Hypothesis p12 : P1 -> P2. + Hypothesis p123 : (P1 -> P2) -> P3. + Hypothesis p34 : P3 -> P4. + + Lemma p14 : P4. + Proof. + eapply strange_imp_trans. + apply modpon. + Abort. +End eex. diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out new file mode 100644 index 0000000000..29ebba7c86 --- /dev/null +++ b/test-suite/output-coqtop/DependentEvars2.out @@ -0,0 +1,120 @@ + +Coq < +Coq < Coq < 1 subgoal + + ============================ + forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R + +(dependent evars: ; in current goal:) + +strange_imp_trans < +strange_imp_trans < No more subgoals. + +(dependent evars: ; in current goal:) + +strange_imp_trans < +Coq < Coq < 1 subgoal + + ============================ + forall P Q : Prop, (P -> Q) /\ P -> Q + +(dependent evars: ; in current goal:) + +modpon < +modpon < No more subgoals. + +(dependent evars: ; in current goal:) + +modpon < +Coq < Coq < +Coq < P1 is declared +P2 is declared +P3 is declared +P4 is declared + +Coq < p12 is declared + +Coq < p123 is declared + +Coq < p34 is declared + +Coq < Coq < 1 subgoal + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + P4 + +(dependent evars: ; in current goal:) + +p14 < +p14 < Second proof: + +p14 < 4 focused subgoals +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?Q -> P4 + +subgoal 2 is: + ?P -> ?Q +subgoal 3 is: + ?P -> ?Q +subgoal 4 is: + ?P + +(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5) + +p14 < 1 focused subgoal +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?Q -> P4 + +(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5) + +p14 < This subproof is complete, but there are some unfocused goals. +Try unfocusing with "}". + +3 subgoals +(shelved: 2) + +subgoal 1 is: + ?P -> (?Goal2 -> P4) /\ ?Goal2 +subgoal 2 is: + ?P -> (?Goal2 -> P4) /\ ?Goal2 +subgoal 3 is: + ?P + +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:) + +p14 < 3 focused subgoals +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?P -> (?Goal2 -> P4) /\ ?Goal2 + +subgoal 2 is: + ?P -> (?Goal2 -> P4) /\ ?Goal2 +subgoal 3 is: + ?P + +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11) + +p14 < +Coq < +Coq < diff --git a/test-suite/output-coqtop/DependentEvars2.v b/test-suite/output-coqtop/DependentEvars2.v new file mode 100644 index 0000000000..d0f3a4012e --- /dev/null +++ b/test-suite/output-coqtop/DependentEvars2.v @@ -0,0 +1,27 @@ +Set Printing Dependent Evars Line. +Lemma strange_imp_trans : + forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R. +Proof. + auto. +Qed. + +Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q. +Proof. + tauto. +Qed. + +Section eex. + Variables P1 P2 P3 P4 : Prop. + Hypothesis p12 : P1 -> P2. + Hypothesis p123 : (P1 -> P2) -> P3. + Hypothesis p34 : P3 -> P4. + + Lemma p14 : P4. + Proof. + idtac "Second proof:". + eapply strange_imp_trans. + { + apply modpon. + } + Abort. +End eex. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index a89fd64999..d48d8b900f 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -38,10 +38,10 @@ Argument scopes are [type_scope _] bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) -foo@{u UnivBinders.17 v} = -Type@{UnivBinders.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1,UnivBinders.17+1,v+1)} -(* u UnivBinders.17 v |= *) +foo@{u UnivBinders.18 v} = +Type@{UnivBinders.18} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.18+1,v+1)} +(* u UnivBinders.18 v |= *) Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) @@ -68,19 +68,19 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.33} in -let ff := Type@{UnivBinders.35} in tt -> ff - : Type@{max(UnivBinders.32,UnivBinders.34)} +let tt := Type@{UnivBinders.34} in +let ff := Type@{UnivBinders.36} in tt -> ff + : Type@{max(UnivBinders.33,UnivBinders.35)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1,M+1,N+1)} (* E M N |= *) -foo@{u UnivBinders.17 v} = -Type@{UnivBinders.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1,UnivBinders.17+1,v+1)} -(* u UnivBinders.17 v |= *) +foo@{u UnivBinders.18 v} = +Type@{UnivBinders.18} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.18+1,v+1)} +(* u UnivBinders.18 v |= *) Inductive Empty@{E} : Type@{E} := (* E |= *) Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } @@ -143,26 +143,26 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.57 UnivBinders.58} : -Type@{UnivBinders.57} -> Type@{i} -(* i UnivBinders.57 UnivBinders.58 |= *) +axfoo@{i UnivBinders.59 UnivBinders.60} : +Type@{UnivBinders.59} -> Type@{i} +(* i UnivBinders.59 UnivBinders.60 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.57 UnivBinders.58} : -Type@{UnivBinders.58} -> Type@{i} -(* i UnivBinders.57 UnivBinders.58 |= *) +axbar@{i UnivBinders.59 UnivBinders.60} : +Type@{UnivBinders.60} -> Type@{i} +(* i UnivBinders.59 UnivBinders.60 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axbar -axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i} +axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo' -axbar' : Type@{axbar'.u0} -> Type@{axbar'.i} +axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out new file mode 100644 index 0000000000..473db2d312 --- /dev/null +++ b/test-suite/output/locate.out @@ -0,0 +1,3 @@ +Notation +"b1 && b2" := if b1 then b2 else false (default interpretation) +"x && y" := andb x y : bool_scope diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v new file mode 100644 index 0000000000..af8b0ee193 --- /dev/null +++ b/test-suite/output/locate.v @@ -0,0 +1,3 @@ +Set Printing Width 400. +Notation "b1 && b2" := (if b1 then b2 else false). +Locate "&&". diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 81469d79c3..fd6101bf89 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq810. +Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index afeb57f9f2..f774cef44f 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(* -*- coq-prog-args: ("-compat" "8.9") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq811. Import Coq.Compat.Coq810. Import Coq.Compat.Coq89. -Import Coq.Compat.Coq88. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..20eef955b4 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq811. +Import Coq.Compat.Coq810. +Import Coq.Compat.Coq89. +Import Coq.Compat.Coq88. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index c8f75915c8..1c5ccc1a92 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq811. Import Coq.Compat.Coq810. -Import Coq.Compat.Coq89. diff --git a/test-suite/success/section_poly.v b/test-suite/success/section_poly.v new file mode 100644 index 0000000000..1e2201f2de --- /dev/null +++ b/test-suite/success/section_poly.v @@ -0,0 +1,74 @@ + + +Section Foo. + + Variable X : Type. + + Polymorphic Section Bar. + + Variable A : Type. + + Definition id (a:A) := a. + +End Bar. +Check id@{_}. +End Foo. +Check id@{_}. + +Polymorphic Section Foo. +Variable A : Type. +Section Bar. + Variable B : Type. + + Inductive prod := Prod : A -> B -> prod. +End Bar. +Check prod@{_}. +End Foo. +Check prod@{_ _}. + +Section Foo. + + Universe K. + Inductive bla := Bla : Type@{K} -> bla. + + Polymorphic Definition bli@{j} := Type@{j} -> bla. + + Definition bloo := bli@{_}. + + Polymorphic Universe i. + + Fail Definition x := Type. + Fail Inductive x : Type := . + Polymorphic Definition x := Type. + Polymorphic Inductive y : x := . + + Variable A : Type. (* adds a mono univ for the Type, which is unrelated to the others *) + + Fail Variable B : (y : Type@{i}). + (* not allowed: mono constraint (about a fresh univ for y) regarding + poly univ i *) + + Polymorphic Variable B : Type. (* new polymorphic stuff always OK *) + + Variable C : Type@{i}. (* no new univs so no problems *) + + Polymorphic Definition thing := bloo -> y -> A -> B. + +End Foo. +Check bli@{_}. +Check bloo@{}. + +Check thing@{_ _ _}. + +Section Foo. + + Polymorphic Universes i k. + Universe j. + Fail Constraint i < j. + Fail Constraint i < k. + + (* referring to mono univs in poly constraints is OK. *) + Polymorphic Constraint i < j. Polymorphic Constraint j < k. + + Polymorphic Definition foo := Type@{j}. +End Foo. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? |