michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/standard/data/int): remove misnamed file

Browse source
This commit is contained in:
Jeremy Avigad 2014-08-21 20:28:16 -07:00 committed by Leonardo de Moura
parent 02fba6e949
commit 1fdc483ab9
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/standard/data/int/int.default
View file

@ -1,5 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad
import .basic