git.annexia.org / goals.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 97494bf) | patch
run: If multiple goals match a tactic, at most one must have a CODE section.
authorRichard W.M. Jones <rjones@redhat.com>
Fri, 3 Jan 2020 15:09:28 +0000 (15:09 +0000)
committerRichard W.M. Jones <rjones@redhat.com>
Fri, 3 Jan 2020 15:16:15 +0000 (15:16 +0000)
commit744ed04530d16567403eccdaf55e479834dbbc0e
treef7567eff067d82cc8cc3f180085e76c849490c51tree | snapshot
parent97494bfc31556510759b0893803d815e3f2a9ad5commit | diff
run: If multiple goals match a tactic, at most one must have a CODE section.

This now works the same way as make.
src/run.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.