HomeIsabelle/Phabricator

Change underlying internal definition of OS.IO.iodesc to use pointer equality…

Description

Change underlying internal definition of OS.IO.iodesc to use pointer equality since it is actually
a byte ref. Using an int as the internal definition uses the wrong equality function and failed in the
new interpreted version.

Details

Provenance
dcjmAuthored on Nov 12 2020, 1:01 PM
Parents
rPOLYML789812541c74: Merge branch 'master' into OriginalBoot
Branches
Unknown
Tags
Unknown