这是indexloc提供的服务,不要输入任何密码
Skip to content

doc: add no_contract flag to index #1341

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Nov 9, 2023
Merged

Conversation

bennn
Copy link
Contributor

@bennn bennn commented Nov 2, 2023

No description provided.

Copy link

@github-actions github-actions bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Resyntax analyzed 0 files in this pull request and found no issues.

@@ -36,4 +36,5 @@ untyped code.
By default, these contracts do not check that typed code obeys the types.
If you want to generate contracts that check both sides equally (for analysis,
for teaching, etc.) then set the environment variable
@envvar{PLT_TR_NO_CONTRACT_OPTIMIZE} to any value and recompile.
@index["PLT_TR_NO_CONTRACT_OPTIMIZE"]{@envvar{PLT_TR_NO_CONTRACT_OPTIMIZE}}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems like this should be supported directly in envvar.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

by default, or with an optional #:index? flag?

@samth
Copy link
Member

samth commented Nov 3, 2023

Probably optional because we don't want to index every place PATH is referenced.

@samth
Copy link
Member

samth commented Nov 9, 2023

I'm going to merge this, but I do think adding to envvar is a good idea.

@samth samth merged commit 7054dac into racket:master Nov 9, 2023
@bennn
Copy link
Contributor Author

bennn commented Nov 9, 2023

oh, thanks for merging!

I'll try to update envvar this month.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants