Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Misc fixes/updates #753

Merged
merged 4 commits into from
Apr 25, 2018
Merged

Misc fixes/updates #753

merged 4 commits into from
Apr 25, 2018

Conversation

ampli
Copy link
Member

@ampli ampli commented Apr 25, 2018

  1. Help file fixes.
  2. ChangeLog: Update about !!idiom_search (PR Dict idioms #747).
  3. Fix typos in comments and READMEs.
  4. Fix typos in 4.0.dict.m4.

@ampli
Copy link
Member Author

ampli commented Apr 25, 2018

I guess this is a typo too:
not_suprisingly

@linas linas merged commit fbae607 into opencog:master Apr 25, 2018
@linas
Copy link
Member

linas commented Apr 25, 2018

"not_surprisingly" ?

@ampli
Copy link
Member Author

ampli commented Apr 25, 2018

"not_surprisingly" ?

I guess so. I can send a PR.

@ampli ampli mentioned this pull request Apr 26, 2018
Merged
@ampli ampli deleted the misc1 branch May 26, 2018 15:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@ampli @linas