diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-04 18:35:54 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-04 16:35:54 -0700 |
| commit | dbe3d6da12fc30eb3bdf00d640e7457fba67e8dc (patch) | |
| tree | 273142b94ba9be3837e062c4df2ca0ff15c64eb4 /src/lib | |
| parent | dd98af783ca7236acca3ee5d5bbcd0bf1df7828a (diff) | |
Remove redundant strings rewrite. (#2422)
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since
re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )
This PR removes the above rewrite, which was implemented incorrectly and was dead code.
Diffstat (limited to 'src/lib')
0 files changed, 0 insertions, 0 deletions