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

Some fix for API. #433

Merged
merged 1 commit into from Feb 15, 2017
Merged

Some fix for API. #433

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
3 changes: 0 additions & 3 deletions doc/indexdoc.client
View file
Open in desktop
Expand Up @@ -3,8 +3,6 @@
{!modules:
Os_current_user
Os_date
Os_email
Os_group
Os_handlers
Os_icons
Os_lib
Expand All @@ -16,7 +14,6 @@ Os_request_cache
Os_services
Os_session
Os_tips
Os_tools
Os_types
Os_user
Os_user_proxy
Expand Down
3 changes: 1 addition & 2 deletions doc/indexdoc.server
View file
Open in desktop
Expand Up @@ -5,6 +5,7 @@ Os_current_user
Os_date
Os_db
Os_email
Os_fcm_notif
Os_group
Os_handlers
Os_icons
Expand All @@ -13,12 +14,10 @@ Os_msg
Os_notif
Os_page
Os_platform
Os_push_notifications
Os_request_cache
Os_services
Os_session
Os_tips
Os_tools
Os_types
Os_uploader
Os_user
Expand Down
1 change: 1 addition & 0 deletions src/os_user_proxy.eliomi
View file
Open in desktop
Expand Up @@ -26,6 +26,7 @@
requests, this last one is implementing only server side. Same for
{!Os_request_cache} which is also only server-side.
*)

[%%server.start]

(** Cache keeping userid and user information as a {!Os_types.user} type. *)
Expand Down