diff options
| author | Maxime Dénès | 2019-05-23 13:52:23 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-23 16:21:50 +0200 |
| commit | 39471db28724f5720868f7a7d1488d81d190ee60 (patch) | |
| tree | 22d921ebb97ddf7837e06b48f1aef817f8dde702 /kernel/genOpcodeFiles.ml | |
| parent | e7628797fc241a4d7a5c1a5675cb679db282050d (diff) | |
Update `Bind Scope` documentation to reflect 3d09e39dd423d81c6af3e991d5b282ea8608646b
The commit mentioned above changed the semantics of `Bind Scope` to
a dynamic binding behavior. It forgot to update the documentation.
Fixes #10064
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions